proposition: Lemma erecdef_unique c f (m := slength c) (p := erecdef_combine h1 h2 h3): echelon c -> slistpl f m -> (forall i, i <c m -> Vg f i = p f (P (Vg c i)) (Q (Vg c i))) -> f = echelon_recdef c.
proof: Proof. move => pa [pb pc] pd. move: (erecdef_prop pa); set g := (echelon_recdef c). move => [qa qb qc]. have fgf: fgraph f by move: pb => []. have dfdg: domain f = domain g by rewrite qb. have mN := (proj2(proj1 (proj1 pa))). apply: fgraph_exten => // i; rewrite dfdg qb -/m => im. have iN:=(NS_inc_nat mN im). move/(NltP mN):im. move: i iN;apply: Nat_induction1 => n nN Hr lt. rewrite (pd _ lt) (qc _ lt). apply:(erecdef_prop1 pa) => // => j ljn. apply: Hr => //; exact: (clt_ltT ljn lt). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq)