proposition: Lemma echelon_of_base_ex1 U V: echelon_of_base scheme_ex1 (slist2 U V) = ((\Po(\Po U)) \times (\Po V)).
proof: Proof. rewrite /echelon_of_base (echelon_ex1_value U V). move: scheme_ex1_ok1 => [ha hb hc _]. rewrite hb /Vl (cpred_pr2 NS5). move: (slist6_prop U V (\Po U) (\Po(\Po U)) (\Po V) ((\Po(\Po U)) \times (\Po V))) => [ _ _ _ [_ _ _]]. done. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq)