proposition: Lemma Tree_to_tree_injective: injective Tree_to_tree.
proof: Proof. elim. + move => n [ m | e | e e'] /= => eq. - by move: (pr2_def eq) => eq'; rewrite (nat_to_B_injective eq'). - by case: card1_nz; move: (pr1_def eq). - by case: card2_nz; move: (pr1_def eq). + move => e0 Hr [ m | e | e e'] /= => eq. - by case: card1_nz; move: (pr1_def eq). - by move: (pr2_def eq) => /Hr ->. - by case: (card_12); move: (pr1_def eq). + move => e0 Hr e1 Hr' [ m | e | e e'] /= => eq. - by case: card2_nz; move: (pr1_def eq). - by case: (card_12); move: (pr1_def eq). move: (pr2_def eq) => eq'. move: (pr1_def eq') => /Hr ->. by move: (pr2_def eq') => /Hr' ->. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq)