fact: Fixpoint eq_bintree (b1 b2 : bintree) : bool := match b1, b2 with | BinLeaf, BinLeaf => true | BinNode l1 r1, BinNode l2 r2 => eq_bintree l1 l2 && eq_bintree r1 r2 | _, _ => false end.
imports: HB(structures) mathcomp(all_ssreflect) tools combclass ordtype