proposition: Lemma oprod_Meqlt a b c: a <o b -> \0o <o c -> (c *o a) <o (c *o b).
proof: Proof. move => /oltP0 [oa ob ab] /oltP0 [oz oc zc]. apply /oltP; fprops; rewrite (oprod_rec_def oc ob); apply /funI_P. exists (J \0o a); aww; rewrite osum0r; fprops. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)