proposition: Lemma echelon_ex1_value U V: echelon_value scheme_ex1 (slist2 U V) = scheme_val1 U V.
proof: Proof. move: scheme_ex1_ok1=> [sa sb sc [E0 E1 E2 E3 [E4 E5]]]. move:(slist2_prop U V) => [[ra rb] rU rV]. move: (slist6_prop U V (\Po U) (\Po(\Po U)) (\Po V) ((\Po(\Po U)) \times (\Po V))). rewrite /= -/(scheme_val1 U V); set F := (scheme_val1 U V). move => [[Fl Fs] F0 F1 [F2 F3 F4 F5]]. have ss: slength F = slength scheme_ex1 by rewrite Fs sb. symmetry;apply: (erecdef_unique1 sa (conj Fl ss)). move: (@succ_nz \2c) (@succ_nz \3c) (@succ_nz \4c) => aa ab ac. have ad:= card2_nz. have ae:= card1_nz. have cp1: (cpred \1c) = \0c by rewrite cpred1. have cp2: (cpred \2c) = \1c by rewrite -(cpred_pr2 NS1) succ_one. have cp3: (cpred \3c) = \2c by apply: (cpred_pr2 NS2). have cp4: (cpred \4c) = \3c by apply: (cpred_pr2 NS3). have cp5: (cpred \5c) = \4c by apply: (cpred_pr2 NS4). rewrite sb => i /(cltSleP NS5) /cle_eqVlt;case. move => -> /=; rewrite E5 F5; aw. by split => //; rewrite /Vl cp4 cp5 F3 F4. move /(cltSleP NS4) /cle_eqVlt;case. move => -> /=; rewrite E4; aw; split => //. by rewrite /Vl cp2 F4 F1. move /(cltSleP NS3) /cle_eqVlt;case. move => -> /=; rewrite E3; aw; split => //. by rewrite /Vl cp3 F3 F2. move /(cltSleP NS2) /cle_eqVlt;case. move: card1_nz => z1;move => -> /=; rewrite E2; aw; split => //. by rewrite /Vl cp1 F2 F0. case /clt2 => -> /=. by rewrite E0; aw; split => //; rewrite F0 /Vl cp1 rU. by rewrite E1; aw; split => //; rewrite F1 /Vl cp2 rV. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq)