proposition: Lemma Ech_product_prop f g (n := slength f) (m:= slength g) (h := Ech_product f g): echelon f -> echelon g -> \0c <c n -> [/\ echelon h, slength h = csucc (n +c m), esize h = cmax (esize f) (esize g) & [/\ forall i, i <c n -> Vg h i = (Vg f i), Vg h (n +c m) = (J n (n +c m)) , forall i, i <c m -> Vg h (n +c i) = ech_shift n (Vg g i) & forall i, n <=c i -> i <c n +c m -> Vg h i = ech_shift n (Vg g (i -c n))]].
proof: Proof. move=> echelon1 echelon2 np. move: (echelon1)(echelon2) =>[[ha1 ha2] ha3] [[hb1 hb2] hb3]. have nz:=(nesym (proj2 np)). have nN: natp n by exact (proj2 ha1). have mN: natp m by exact (proj2 hb1). have nmN := (NS_sum nN mN). have snmN:= (NS_succ nmN). have cp1:= (Nsum_M0le m nN). have cp2 :=(cleR (CS_nat nmN)). have r0 i: i <c n +c m -> inc i (csucc (n +c m)). move => lin; apply/(NltP snmN). exact:(clt_leT lin (cleS nmN)). have r1 i: i <c n -> Vg h i = Vg f i. move => lin. move: (ech_product_prop1 f g i nN mN) => [<- // _ _ ]. rewrite /h /Ech_product LgV//; aw; apply: r0. exact:(clt_leT lin cp1). have r2: Vg h (n +c m) = J n (n +c m). rewrite /h /Ech_product LgV; last by rewrite (succ_of_nat nmN);fprops. by case:(ech_product_prop1 f g n nN mN). have r3 i: i <c m -> Vg h (n +c i) = ech_shift n (Vg g i). move => min; rewrite /h /Ech_product LgV//. by move: (ech_product_prop1 f g i nN mN) => [ _ _ ->]. apply: r0;apply:(csum_Meqlt nN min). have r4 i: n <=c i -> i <c n +c m -> Vg h i = ech_shift n (Vg g (i -c n)). move => i1 i2; move:(NS_lt_nat i2 nmN)(cdiff_pr i1) => iN i3. move: i2; rewrite -{1 2} i3 => i2. by move: (csum_lt2l nN (NS_diff n iN) mN i2) => i4; rewrite r3. have r5: slength h = csucc (n +c m). by rewrite /slength /h /Ech_product Lgd. have r6: sub (range h) (Nat \times Nat). move => t /Lg_range_P [b bs ->]. move: (ech_product_prop1 f g b nN mN) => [sa sb sc]. move/(NltP snmN): bs => /(cltSleP nmN) /cle_eqVlt []. by move => ->; rewrite sb; apply: setXp_i. move => lbnm; case:(cleT_el (CS_nat nN) (proj31_1 lbnm)) => lbn; last first. rewrite (sa lbn); apply: ha2; apply /(range_gP (proj1 ha1)); exists b=> //. by apply /(NltP nN). move: (cdiff_pr lbn) => d1. have bN:= (NS_lt_nat lbnm nmN). rewrite - d1 in lbnm; move: (csum_lt2l nN (NS_diff n bN) mN lbnm) => ha. move: (ech_product_prop1 f g (b -c n) nN mN) => [_ _ sc']. rewrite - d1 (sc' ha); rewrite /ech_shift. have vr : inc (Vg g (b -c n)) (range g). by apply /(range_gP (proj1 hb1)); exists (b-c n) => //;apply /(NltP mN). move: (hb2 _ vr) =>w. move/setX_P: (w)=>[]; set aa := P _; set bb :=Q _ => [qa qb qc]. Ytac h1 => //; Ytac h2. apply:(setXp_i (NS_sum qb nN) NS0). apply:(setXp_i (NS_sum qb nN) (NS_sum qc nN)). have r7: domain h = csucc (n +c m) by rewrite /h/Ech_product; aw. have r8: slist_E h (Nat \times Nat). split => //; split; [ apply:Lg_fgraph | ue]. have r9: echelon h. split => // i; rewrite r5; move => /(cltSleP nmN) /cle_eqVlt []. move => -> /=; rewrite r2; aw;split. by move/csum_nz => [/nz]. move => ha hb; split; split => //; apply/cge1P => //. by apply:(card_ne0_pos (CS_nat nmN)). move => lbnm; case:(cleT_el (CS_nat nN) (proj31_1 lbnm)) => lbn; last first. by rewrite (r1 _ lbn); apply: ha3. move:(NS_lt_nat lbnm nmN)(cdiff_pr lbn) => iN i3. move: lbnm; rewrite -{1 2 3} i3 => i2. move: (csum_lt2l nN (NS_diff n iN) mN i2) => i4. move:(hb3 _ i4); rewrite (r3 _ i4) /ech_shift /=. set a := P _; set b := Q _; move => [ha hb]. case:(equal_or_not a \0c) => az; Ytac0. split; first by move/ha => []; rewrite az => a1; move:(cltNge clt_01 a1). by move => _; case. have h0 c: ech_good c (i -c n) -> ech_good (c +c n) i. move => [hc hd]; split; first exact: (cleT hc (csum_M0le n (proj32 hc))). by rewrite - i3 csumC; apply: csum_Meqle. case:(equal_or_not b \0c) => bz; Ytac0; aw; split. - by move => _; move: (ha bz); apply: h0. - by case. - by move /csum_nz => [_ /nz]. - by move:(hb bz az) => [hc hd] _ _; split; apply: h0. split => //. move: (esize_prop1 echelon1 np); set N := esize f. move => [NN Np [ja ja1 ja2] ja3]. case: (equal_or_not m \0c) => mz. have max0: cmax N \0c = N. by rewrite (cmax_yx (proj1 Np)). rewrite (esize_empty echelon2 mz) max0. have s0: slength h = csucc n. by rewrite /slength r7 mz (csum0r (CS_nat nN)). apply: (esize_prop2 r9); rewrite s0. exists ja; [exact:(clt_leT ja1 (cleS nN)) | by rewrite r1]. move => j /(cltSleP nN) /cle_eqVlt []. move ->. move: r2. rewrite mz (csum0r (CS_nat nN)) => ->; aw => //. move => jn; rewrite (r1 _ jn); exact (ja3 _ jn). have mp:= (card_ne0_pos (CS_nat mN) mz). move: (esize_prop1 echelon2 mp); set M := esize g. move => [MN Mp [ka ka1 ka2] ka3]. move:(cmax_p1 (proj32_1 Np) (proj32_1 Mp)) => [max1 max2]. apply: (esize_prop2 r9). have ja4: ja <c slength h. rewrite r5; exact: (clt_leT (clt_leT ja1 cp1) (cleS nmN)). have ka4: n +c ka <c slength h. rewrite r5; exact: (clt_leT (csum_Meqlt nN ka1) (cleS nmN)). rewrite /cmax/Gmax; case: (p_or_not_p (N <=c M)) => lnm; Ytac0. exists (n +c ka) => //;rewrite (r3 _ ka1). by rewrite /ech_shift ka2 pr1_pair (Y_true (erefl \0c)). by exists ja => //;rewrite r1. move => j; rewrite r5; move => /(cltSleP nmN) /cle_eqVlt []. by move => -> /=; rewrite r2; aw. move => ljnm; case:(cleT_el (CS_nat nN) (proj31_1 ljnm)) => ljn; last first. rewrite (r1 _ ljn) => anz; exact: (cleT (ja3 _ ljn anz) max1). move:(NS_lt_nat ljnm nmN)(cdiff_pr ljn) => iN i3. move: ljnm; rewrite -{1 2 3} i3 => i2. move: (csum_lt2l nN (NS_diff n iN) mN i2) => i4. rewrite (r3 _ i4) /ech_shift; set a:= (P (Vg g _)); set b := Q _. case:(equal_or_not a \0c) => az; Ytac0. move => _; exact: (cleT (ka3 _ i4 az) max2). have anz : a +c n <> \0c by move/csum_nz => []. by case:(equal_or_not b \0c) => bz; Ytac0; aw. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq)