proposition: Lemma Exercise2_6i: inductive r -> exists2 a, inc a (source f) & Vf f a = a.
proof: Proof. move => ir; move: (Zorn_lemma or ir) => [a [asr am]]. rewrite - sf;exists a;fprops. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)