proposition: Theorem and_cancel_r : forall A B C : Prop, (B -> A) -> (C -> A) -> ((B /\ A <-> C /\ A) <-> (B <-> C)).
proof: Proof. intros A B C Hl Hr. split; [ | apply and_iff_compat_r]; intros [HypL HypR]; split; intros. + apply HypL; split; [ | apply Hl ]; assumption. + apply HypR; split; [ | apply Hr ]; assumption. Qed.
imports: Notations Ltac