proposition: Lemma ord_negl_prodr a b c: ordinalp a -> ordinalp b -> ordinalp c -> a <<o b -> c *o a <<o (c *o b).
proof: Proof. by move => oa ob oc; rewrite /ord_negl - (oprodD oa ob oc) => ->. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)