proposition: Lemma cancel_inj `{Cancel A B R1 f g, !Equivalence R1, !Proper (R2 ==> R1) f} : Inj R1 R2 g.
proof: Proof. intros x y E. rewrite <-(cancel f g x), <-(cancel f g y), E. reflexivity. Qed.
imports: Coq(Permutation) Coq.ssr((notations) ssrfun) stdpp(options)