proposition: Lemma ex9_propa x y: inc x ex9_G -> inc y ex9_G -> ex9_rel x y -> ex9_srel x y.
proof: Proof. move => /ex9G_P [px Px Qx] /ex9G_P [py Py Qy] [qa qb]. have: gle r (Q y) (Q y) by apply: (proj32 or); rewrite sr. by exists (Q y); split => //; rewrite - qb (identity_f Py) idV. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)