proposition: Lemma mx_dot_leq n m p: Proper (leq ==> leq ==> leq) (mx_dot X u n m p).
proof: Proof. intros ? ? H ? ? H' i j. apply sup_leq; trivial. intro k. apply dot_leq. apply H. apply H'. Qed.
imports: comparisons kleene sums normalisation