proposition: Lemma not_inj2_1 `{Inj2 A B C R R' R'' f} x1 x2 y1 y2 : ¬R x1 x2 → ¬R'' (f x1 y1) (f x2 y2).
proof: Proof. intros HR HR''. destruct (inj2 f x1 y1 x2 y2); auto. Qed.
imports: Coq(Permutation) Coq.ssr((notations) ssrfun) stdpp(options)