proposition: Lemma echelon_trivial n (S:= slist1 (J \0c n)): natp n -> n <> \0c -> echelon S /\ esize S = n.
proof: Proof. move: NS0 clt_01=> ns0 lt01 nN np. move: (slist1_prop (J \0c n)) => [[ha hb] hc]. have es: echelon S. split; first by split => // t /Lg_range_P [_ _ ->]; apply:setXp_i. by rewrite hb => i /clt1 ->; rewrite hc /=; aw; split. split => //; apply: (esize_prop2 es); rewrite hb; first by exists \0c. move => j /clt1->; rewrite hc pr2_pair => _; exact: (cleR (CS_nat nN)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq)