proposition: Lemma scheme_ex2_ok1 (E := scheme_ex2): [/\ echelon E, slength E = \6c, esize E = \2c & [/\ Vg E \0c = J \0c \2c, Vg E \1c = J \0c \1c, Vg E \2c = J \1c \0c, Vg E \3c = J \2c \0c& (Vg E \4c =J \4c \0c /\ Vg E \5c =J \5c \3c) ]].
proof: Proof. move: NS0 NS1 NS2 NS3 NS4 NS5 NS6 => ns0 ns1 ns2 ns3 ns4 ns5 ns6. move: (slist6_prop (J \0c \2c) (J \0c \1c) (J \1c \0c) (J \2c \0c) (J \4c \0c) (J \5c \3c)). rewrite /= -/ scheme_ex2 -/E. move => [[ha sE] E0 E1 [E2 E3 E4 E5]]. have rE:slist_E E (Nat \times Nat). split; first exact. move => i /Lg_range_P [b bN ->]; Ytac h1;first by apply:setXp_i. Ytac h2; first by apply:setXp_i. Ytac h3; first by apply:setXp_i. Ytac h4; first by apply:setXp_i. by Ytac h5; apply:setXp_i. move:clt_5 => [lt05 lt15 lt25 lt35 lt45]. move:clt_4 => [lt04 lt14 lt24 lt34]. move:clt_3 => [lt03 lt13 lt23]. move: (proj1 clt_12) => cle_12. have EE: echelon E. split => //; rewrite sE => i /(cltSleP ns5) /cle_eqVlt;case. move: (proj1 lt13) (proj1 lt35) (proj1 lt15) => ua ub uc. have ra:ech_good \3c \5c by split. have rb: ech_good \5c \5c by split; fprops. by move => ->; rewrite E5; simpl; aw. move /(cltSleP ns4) /cle_eqVlt;case. move => ->; rewrite E4 /=; aw; split => // _. split; [ exact: (proj1 lt14) | fprops]. move /(cltSleP ns3) /cle_eqVlt;case. move => ->; rewrite E3 /=; aw; split => //_. split; [ exact | exact: (proj1 lt23)]. move /(cltSleP ns2) /cle_eqVlt;case. move => ->; rewrite E2 /=; aw ; split => //_; split; fprops. case /clt2 => ->. by move: (card2_nz) => ra; rewrite E0 /=; aw; split. by move: (card1_nz) => ra; rewrite E1 /=; aw; split. split => //. move:(clt_6) => [l06 l16 l26 l36 [l46 l56]]. have sp: \0c <c slength E by rewrite sE. move: (esize_prop1 EE sp); set n := esize E. move => [ra rb rc rd]. apply: cleA; last first. have ww: \0c <c slength E by ue. by move: (rd _ ww); rewrite E0; aw; apply. move: rc =>[j]; rewrite sE;move /(cltSleP ns5) /cle_eqVlt;case. move ->; rewrite E5 => /(f_equal P); aw => e50. by case:(proj2 lt05). move /(cltSleP ns4) /cle_eqVlt;case. move => ->; rewrite E4 => /(f_equal P); aw => e40. by case:(proj2 lt04). move /(cltSleP ns3) /cle_eqVlt;case. by move => ->; rewrite E3 => /(f_equal P); aw => /card2_nz. move /(cltSleP ns2) /cle_eqVlt;case. by move => ->; rewrite E2 => /(f_equal P); aw => z3; case: card1_nz. case /clt2 => ->; rewrite ?E0 ? E1; move /(f_equal Q); aw => <-; fprops. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq)