proposition: Lemma erecdef_prop c (m := slength c)(f := echelon_recdef c) (p := erecdef_combine h1 h2 h3): echelon c -> [/\ fgraph f, domain f = m & forall i, i <c m -> Vg f i = p f (P (Vg c i)) (Q (Vg c i))].
proof: Proof. move => ec; move: (ec)=> [[ka kb] kc]. rewrite /f /echelon_recdef{f}; set g := fun u:Set => _. move: Nat_order_wor => [wor sr]. move: (transfinite_defined_pr g wor). set f1 := (transfinite_defined Nat_order g). rewrite /transfinite_def sr /g; move => [ra rb rc]. have sa i: natp i -> Vf f1 i = p (restr (graph f1) i)(P (Vg c i))(Q (Vg c i)). move => iN; rewrite (rc _ iN) /restriction1. by rewrite (segment_Nat_order iN) (NintE iN); aw. move: (slength_nat ka); rewrite -/m => mN. set f := restr _ _. have ha: fgraph f by apply: restr_fgraph. have hb: domain f = m by rewrite /f restr_d. split => // i lim. have iN:= (NS_lt_nat lim mN). have il: inc i m by apply /(NltP mN). rewrite /f (restr_ev _ il) -/(Vf _ _) (sa _ iN); apply: (erecdef_prop1 ec) => // j ji. have ijm: inc j m by apply /(NltP mN); apply: (clt_ltT ji lim). have iji: inc j i by apply /(NltP iN). by rewrite !LgV. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq)