proposition: Lemma tree_to_pos_p2: [/\ (forall x, natp x -> (tree_is_pos (Tb x) <-> x <> \0c)), (forall x, treep x -> (tree_is_pos (Tp x) <-> tree_is_pos x)) & (forall x x', treep x -> treep x' -> (tree_is_pos (Tx x x') <-> ((tree_is_pos x) /\ (tree_is_pos x'))))].
proof: Proof. rewrite /tree_is_pos;split. - move => n nN; case: (equal_or_not n \0c) => nz. rewrite nz; move:(tree_to_pos_p1) => [_ -> _ _]; split => // w. by case:card1_nz. have [sa sb]:= (cpred_pr nN nz); rewrite sb. move:(tree_to_pos_p1) => [sc _ _ _]; rewrite (sc _ sa); split => //. by move => _; apply: succ_nz. - by move => x xT; move:(tree_to_pos_p1) => [_ _ sc _]; rewrite (sc _ xT). - move => x x' xT xT'. move: (tree_to_pos_p1) => [_ _ _ sd]; rewrite (sd _ _ xT xT'). split; last by move => [-> ->]; rewrite /cmin/Gmin; Ytac w. have ha: forall x, natp x -> (fun n => Yo (n = \0c) \0c \1c) x <=c \1c. move => n nN /=; Ytac w; [ exact: cle_01 | exact (cleR CS1)]. move: (tree_rec_bool ha xT) (tree_rec_bool ha xT'). rewrite -/tree_to_pos /cmin/Gmin; move => ra rb. Ytac w => vv; split => //;apply: cleA => //; rewrite - vv //. by move:w;rewrite vv; case. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq)