proposition: Lemma oprod_Mleeq a b c: a <=o b -> ordinalp c -> (a *o c) <=o (b *o c).
proof: Proof. move => [oa ob sab]; move: c; apply: least_ordinal2' => d od H. split; fprops. rewrite (oprod_rec_def oa od) => t /funI_P [z /setX_P [_ p2 p3] ->]. apply: (ole_ltT_s (OS_prod2 ob od) (osum_Mleeq (H _ p3) (Os_ordinal oa p2))). rewrite (oprod_rec_def ob od); apply /funI_P; exists (J (P z) (Q z));aww. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)