proposition: Lemma prod_mono : monotone (f1 \* f2).
proof: Proof. by case=>x1 x2 [y1 y2][/= H1 H2]; split; [apply: M1 | apply: M2]. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun ssrnat eqtype seq) pcm(options axioms pred prelude)