proposition: Lemma oprod2_simpl a b c: ordinalp a -> ordinalp b -> \0o <o c -> c *o a = c *o b -> a = b.
proof: Proof. move=> oa ob oc eq. by case: (oleT_ell oa ob) => h //; move: (oprod_Meqlt h oc); rewrite eq; move=> [_]; case. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)