proposition: Lemma echelon_to_trees_prop c (m := slength c)(f := echelon_to_trees c) (n := esize c): echelon c -> [/\ fgraph f, domain f = m, forall i, i <c m -> treep (Vg f i) & forall i, i <c m -> let a:= P (Vg c i) in let b := Q (Vg c i) in [/\ a = \0c -> [/\ \1c <=c b, b <=c n & Vg f i = Tb (cpred b)], b = \0c -> [/\ \1c <=c a, a <=c i & Vg f i = Tp (Vl f a)] & a <> \0c -> b <> \0c -> [/\ \1c <=c a, a <=c i, \1c <=c b, b <=c i & Vg f i = Tx (Vl f a) (Vl f b)]]].
proof: Proof. move => ha. move: (erecdef_prop (fun b => Tb (cpred b)) Tp Tx ha) => [hc hd _]. move: (erecdef_prop2 (fun b => Tb (cpred b)) Tp Tx ha) => he. split => //. move => i lim; move:(NS_lt_nat lim (proj2 (proj1 (proj1 ha)))) => iN. move: i iN lim; apply: Nat_induction1. move => i iN Hr lim. move:(he _ lim) => [ra rb rc]. case: (equal_or_not (P (Vg c i)) \0c) => az. move:(ra az) => [sa sb ->]. apply: (TS_base (proj31(cpred_pr6' (NS_esize ha) sa sb))). case: (equal_or_not (Q (Vg c i)) \0c) => bz. move:(rb bz) => [sa sb ->]; have sc := (proj33(cpred_pr6' iN sa sb)). apply:TS_powerset; apply: Hr => //; exact:(clt_ltT sc lim). move:(rc az bz) => [sa sb sa' sb' ->]. have sc := (proj33(cpred_pr6' iN sa sb)); have sd:= (clt_ltT sc lim). have sc' := (proj33(cpred_pr6' iN sa' sb')); have sd':= (clt_ltT sc' lim). by apply:TS_product; apply:Hr. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq)