proposition: Lemma ordinals_Mlt r a b: worder_rc r -> (non_coll (fun x => r x x)) -> a <o b -> (r (ordinals r a) (ordinals r b) /\ (ordinals r a) <> (ordinals r b)).
proof: Proof. move => pa pb [pc pd]; move:(ordinals_Mle pa pb pc) => h. split => // sv. move: (pc) => [oa ob _]. case: pd. rewrite - (proj2 (ordinalsP pa (ordinals_non_coll1 pa pb oa))). by rewrite - (proj2 (ordinalsP pa (ordinals_non_coll1 pa pb ob))) sv. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)