proposition: Lemma lemma_congruenceflip : forall A B C D, Cong A B C D -> Cong B A D C.
proof: Proof. intros. assert (Cong B A A B) by (auto using cn_equalityreverse). assert (Cong C D D C) by (auto using cn_equalityreverse). assert (Cong B A C D) by (conclude lemma_congruencetransitive). conclude lemma_congruencetransitive. Qed.
imports: GeoCoq.Axioms.tarski_axioms GeoCoq.Elements.OriginalProofs.proposition_01 GeoCoq.Elements.OriginalProofs.lemma_congruenceflip GeoCoq.Elements.OriginalProofs.lemma_extension Classical