proposition: Lemma mx_cnv_ext n m (M: mx n m): M ≦ M⋅M°⋅M.
proof: Proof. intros i j. simpl. unfold mx_dot, mx_cnv. setoid_rewrite dotsumx. rewrite <- (leq_xsup _ _ i) by apply in_seq. rewrite <- (leq_xsup _ _ j) by apply in_seq. apply cnv_ext. Qed.
imports: comparisons kleene sums normalisation