proposition: Lemma echelon_p1 c: echelon c -> \0c <c slength c -> exists b, [/\ natp b, \0c <c b & Vl c \1c = J \0c b].
proof: Proof. move => [pa pb] pc. have nN:= (proj2 (proj1 pa)). move/cge1P: pc => ha. move /setX_P: (Vl_p1 pa (cleR CS1) ha) => [ra rb rc]. have pd: \0c <c slength c by apply/(cleSltP NS0); rewrite succ_zero. move: (pb _ pd); simpl; move /setX_P: (Vl_p1 pa (cleR CS1) ha). rewrite /Vl cpred1; set a:= P _; set b := Q _; move => [sa sb sc] [sd se]. have Ha w: ech_good w \0c -> False. by move => [la lb]; move: (cltNge clt_01) (cleT la lb). case(equal_or_not b \0c) => bz; first by move: (Ha _ (sd bz)). case(equal_or_not a \0c) => az; last by case: (Ha _ (proj1 (se bz az))). have bp:= (card_ne0_pos (CS_nat sc) bz). by exists b; rewrite - sa -/a az. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq)