proposition: Lemma set_lt_notP a b: ~(a <s b) <-> (forall f, injection_prop f a b -> a \Eq b).
proof: Proof. split => H; last by case; case => f /H. by move => f fp; ex_middle bad; case:H; split => //; exists f. Qed.
imports: mathcomp(ssreflect ssrbool eqtype ssrfun)