proposition: Lemma tdepth_prop_inv: [/\ forall n, natp n -> treep (Tb n) /\ tdepth (Tb n) = \0c, forall t, treep t -> treep (Tp t) /\ tdepth (Tp t) = csucc (tdepth t) & forall t t', treep t -> treep t' -> treep (Tx t t') /\ tdepth (Tx t t') = csucc (cmax (tdepth t) (tdepth t')) ].
proof: Proof. split. - move =>n nN. have xb0: inc (Tb n) (tset_index \0c). by rewrite tset_index0; apply:tset_basei. move: (tdepth3 NS0 xb0) => /cle0 tz. split => //; apply/tsetP; exists \0c => //; exact: NS0. - move => t tS; move: (tdepth1 tS) => [sa sb sc]. have sd := (NS_succ sa). have tsn: inc (Tp t) (tset_index (csucc (tdepth t))). by rewrite (tset_indexS sa); apply/tset_nextP; constructor 1; exists t. have nts: treep (Tp t) by apply/tsetP; exists (csucc (tdepth t)). split => //; move: (tdepth3 sd tsn) => le1. case: (equal_or_not (tdepth (Tp t)) \0c) => tnz. by move:(tdepth4 nts tnz) => /tset_baseP [n nN /pr1_def e01]; case:card1_nz. move: (cpred_pr (NS_le_nat le1 sd) tnz) => [ma mb]. case: (tdepth_prop nts ma mb). move => [y [ya yb /pr2_def yc]]; apply: cleA => //. by rewrite mb {1} yc; apply: cleSS. by move => [y [z [_ _ _ _ /pr1_def eq12]]]; case: card_12. - move => t t' tS tS'; move: (tdepth1 tS)(tdepth1 tS')=> [sa sb sc][ra rb rc]. case: (Nmax_p1 sa ra). set m := (cmax (tdepth t) (tdepth t')) => mN max1 max2. have smN:= (NS_succ mN). have tsn: inc (Tx t t') (tset_index (csucc m)). rewrite (tset_indexS mN); apply/tset_nextP; constructor 2; exists t, t'. by split=>//; [apply: (tdepth2 tS mN max1) | apply: (tdepth2 tS' mN max2) ]. have nts: treep (Tx t t') by apply/tsetP; exists (csucc m). split => //. move: (tdepth3 smN tsn) => le1. case:(equal_or_not (tdepth (Tx t t')) \0c) => tnz. by move:(tdepth4 nts tnz)=> /tset_baseP [n nN /pr1_def e02]; case: card2_nz. move: (cpred_pr (NS_le_nat le1 smN) tnz) => [ma mb]. case: (tdepth_prop nts ma mb). by move => [y [_ _ /pr1_def eq12]]; case: card_12. move => [y [z [ yT zT dy dz /pr2_def eq1]]]; apply:cleA => //. rewrite mb; apply:cleSS. by move: (cmax_p0 dy dz); rewrite -(pr1_def eq1) - (pr2_def eq1) -/m mb. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq)