proposition: Lemma cprod_Mlele a b a' b': a <=c a' -> b <=c b' -> (a *c b) <=c (a' *c b').
proof: Proof. by move=> aa' bb';apply: cprod_increasing;aww => x xtp; try_lvariant xtp. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)