proposition: Lemma erecdef_product c c' (c'' := Ech_product c c'): echelon c -> echelon c' -> \0c <c slength c -> \0c <c slength c' -> echelon_recdef_last c'' = h3 (echelon_recdef_last c) (echelon_recdef_last c').
proof: Proof. rewrite/echelon_recdef_last => ec ec' cp cp'. move:(Ech_product_prop ec ec' cp) => [ra rb rc [rd re rf rg]]. move:(proj2 (proj1 (proj1 ec))) (proj2 (proj1 (proj1 ec'))) => s1N s2N. move: (CS_nat s1N) (CS_nat s2N) => cs1 cs2. set s := (slength c). set s' := (slength c'); move:(nesym (proj2 cp')) => s2nz. move: (cpred_pr s2N s2nz); rewrite -/(slength c');move => [qa qb]. have eqa:cpred (s +c s') = s +c cpred s'. by rewrite /s' {1} qb (csum_via_succ _ (CS_nat qa)) (cpred_pr1 (CS_sum2 _ _)). have qc: s <=c slength c''. by rewrite rb -(csum_via_succ _ cs2);apply:csum_M0le cs1. have qd: (cpred (slength c'')) = s +c s' by rewrite rb cpred_pr1; fprops. have pa: s <> \0c by exact:(nesym (proj2 cp)). have pb: s +c s' <> \0c by case/csum_nz. have sl1: (cpred (slength c'')) <c (slength c''). apply:(cpred_lt (proj2 (proj1(proj1 ra))));rewrite [domain _]rb. apply: succ_nz. move:(proj33 (erecdef_prop2 ra sl1)); rewrite qd re /Vl; aw => h11. move:(h11 pa pb) => [pc pd pe pf pg] {h11};rewrite /Vl qd pg; congr h3. apply:(echelon_recdef_extent2 ra ec qc (cleR cs1) (nesym (proj2 cp))). by move => k kl; rewrite rd. clear pa pb pc pd pe pf pg. rewrite eqa. have: cpred s' <c s' by exact:(cpred_lt s2N s2nz). move: qa; move: (cpred s'); apply: Nat_induction1. move => i iN Hr lis1. move:( erecdef_prop2 ec' lis1) => [ca cb cc]. have lis2: (s +c i) <c slength (Ech_product c c'). rewrite rb -/s - (csum_via_succ _ cs2); apply:(csum_Meqlt s1N). exact: (clt_leT lis1 (cleS s2N)). move:(erecdef_prop2 ra lis2) => []. rewrite (rf _ lis1) /ech_shift. case: (equal_or_not (P (Vg c' i)) \0c) => az; Ytac0. by move => hu _ _; move: (hu az) (ca az) => [_ _ ->] [_ _ ->]. case: (equal_or_not (Q (Vg c' i)) \0c) => bz; Ytac0. move => _ hu _; move: hu; aw => hu. move: (hu (erefl \0c)) (cb bz) => [p1 p2 ->] [p3 p4 ->]. rewrite /Vl. move: (cpred_pr6' iN p3 p4) => [ua ub uc]. have ->: cpred (P (Vg c' i) +c slength c) = s +c cpred (P (Vg c' i)). rewrite {1} ub csumC (csum_via_succ _ (CS_nat ua)) cpred_pr1; fprops. rewrite Hr //; apply: (clt_ltT uc lis1). move => _ _ hu; move: hu; aw => hu. have az': P (Vg c' i) +c slength c <> \0c by case/csum_nz. have bz': Q (Vg c' i) +c slength c <> \0c by case/csum_nz. move: (cc az bz) => [p1 p2 p3 p4 ->]. move: (hu az' bz') => [p1' p2' p3' p4' ->]. rewrite /Vl. move: (cpred_pr6' iN p1 p2) => [ua ub uc]. have ->: cpred (P (Vg c' i) +c slength c) = s +c cpred (P (Vg c' i)). rewrite {1} ub csumC (csum_via_succ _ (CS_nat ua)) cpred_pr1; fprops. move: (cpred_pr6' iN p3 p4) => [ua' ub' uc']. have ->: cpred (Q (Vg c' i) +c slength c) = s +c cpred (Q (Vg c' i)). rewrite {1} ub' csumC (csum_via_succ _ (CS_nat ua')) cpred_pr1; fprops. move: (clt_ltT uc lis1) (clt_ltT uc' lis1) => lt1 lt2. rewrite Hr // Hr //. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq)