proposition: Lemma pr1_ne2_hyp3_weak_prop: pr1_ne2_hyp3_plain -> pr1_ne2_hyp3_weak.
proof: Proof. move => hp a M aI Mb [x xM]; exists x => // b leab. by apply:hp => //; move: (FS_range aI) => h; move /setP_P:(h _ Mb); apply. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)