proposition: Lemma ex9_propb: reflexive_re ex9_rels ex9_G.
proof: Proof. move => x; split. move => h; split => //; left. move/ex9G_P: h => [px Qx Px]. have g: gle r (Q x) (Q x) by apply: (proj32 or); rewrite sr. by split => //; rewrite (identity_f Qx) idV. by case. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)