proposition: Lemma tree_to_pos_p1: [/\ (forall x, natp x -> tree_to_pos (Tb (csucc x)) = \1c), (tree_to_pos (Tb \0c) = \0c), (forall x, treep x -> tree_to_pos (Tp x) = tree_to_pos x) & (forall x x', treep x -> treep x' -> tree_to_pos (Tx x x') = cmin (tree_to_pos x) (tree_to_pos x'))].
proof: Proof. rewrite /tree_to_pos; split. - move => x xN. have ha:= (tset_basei (NS_succ xN)). by rewrite tree_recdef_pb // pr2_pair Y_false //; exact: succ_nz. - by rewrite (tree_recdef_pb _ _ _ (tset_basei NS0)) pr2_pair Y_true. - by move => x xT; rewrite tree_recdef_pp. - by move => x y xT yT;rewrite tree_recdef_px. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq)