proposition: Lemma ordinals_Mle r a b: worder_rc r -> (non_coll (fun x => r x x)) -> a <=o b -> r (ordinals r a) (ordinals r b).
proof: Proof. move => ha hb ab. move: (ordinalsP ha (ordinals_non_coll1 ha hb (proj31 ab))). move: (ordinalsP ha (ordinals_non_coll1 ha hb (proj32 ab))). set sa := (ordinals r a); set sb := (ordinals r b). move => [rbb vb][raa va]. case: (worderr_total (proj1 ha) raa rbb) => // h. move:(ordinalr_Mle ha h); rewrite va vb => ba. by move: raa; rewrite /sa /sb (oleA ab ba). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)