proposition: Lemma inj_iff {A B} {R : relation A} {S : relation B} (f : A → B) `{!Inj R S f} `{!Proper (R ==> S) f} x y : S (f x) (f y) ↔ R x y.
proof: Proof. firstorder. Qed.
imports: Coq(Permutation) Coq.ssr((notations) ssrfun) stdpp(options)