Additional library which depends on SSReflect (by my ad-lib coding).
(compatible with ssreflect-1.5 and coq-8.4pl4)
About (Japanese Only)
Type of binary tree and some utility functions are defined.
And some properties are proved (in progress)
(will be written)
Tree & Forest (tree.v)
Types of tree and forest are defined by using mutual inductive definition.