proposition: Lemma collectivising_srel_ord (r:relation): (forall x y, r x y -> x <=o y) -> collectivising_srel r.
proof: Proof. move => h1 x /h1 xx. have ox:= (proj31 xx). exists (Zo (osucc x) (r^~ x)); move => y;split; first by move /Zo_hi. by move => ryx; apply:Zo_i => //; apply /(oleP ox); apply: h1. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)