proposition: Lemma lmat_le_decr m n (A B : 'M_(m, n)) : A <=m B -> (A == B) || (num_stars A < num_stars B).
proof: Proof. move=> Hle. suff : (num_stars A <= num_stars B) && ((num_stars A == num_stars B) ==> \big[andb/true]_(i < m) (row i A == row i B)). case/andP => A_le_B. case/boolP : (_ == _) => [A_eq_B|A_not_B _] /=. rewrite big_all => Hall. apply/orP; left. apply/eqP/row_matrixP => i. move/allP/(_ i) : Hall. by rewrite mem_index_enum => /(_ isT)/eqP. by rewrite ltn_neqAle A_le_B A_not_B orbT. rewrite /num_stars. elim/big_ind3 : _ => //. by apply Kop_proof. move=> i _. set lft := (_ <= _). set rgt := (_ == _). suff : lft && (rgt ==> \big[andb/true]_(j < n) (A i j == B i j)). rewrite /lft /rgt. case/andP => ->. case/boolP : (_ == _) => ? //=. rewrite big_all => Hall. apply/eqP/rowP => j. move/allP/(_ j): Hall. by rewrite mem_index_enum !mxE => /(_ isT)/eqP. rewrite /lft /rgt. elim/big_ind3 : _ => //. apply Kop_proof. move=> j _. move/'forall_forallP : Hle => /(_ i j). by case/letterP : (A i j); case/letterP : (B i j). Qed.
imports: mathcomp(all_ssreflect ssralg fingroup finalg perm zmodp) mathcomp(matrix) ssr_ext ssralg_ext num_occ f2 ssrR hamming tanner linearcode