Require Export GeoCoq.Elements.OriginalProofs.lemma_congruencetransitive.

Section Euclid.

Context `{Ax:euclidean_neutral}.

Lemma lemma_congruenceflip : 
   forall A B C D, 
   Cong A B C D ->
   Cong B A D C /\ Cong B A C D /\ Cong A B D C.
Proof.
(* Goal: forall (A B C D : @Point Ax) (_ : @Cong Ax A B C D), and (@Cong Ax B A D C) (and (@Cong Ax B A C D) (@Cong Ax A B D C)) *)
intros.
(* Goal: and (@Cong Ax B A D C) (and (@Cong Ax B A C D) (@Cong Ax A B D C)) *)
assert (Cong B A A B) by (conclude cn_equalityreverse).
(* Goal: and (@Cong Ax B A D C) (and (@Cong Ax B A C D) (@Cong Ax A B D C)) *)
assert (Cong C D D C) by (conclude cn_equalityreverse).
(* Goal: and (@Cong Ax B A D C) (and (@Cong Ax B A C D) (@Cong Ax A B D C)) *)
assert (Cong B A C D) by (conclude lemma_congruencetransitive).
(* Goal: and (@Cong Ax B A D C) (and (@Cong Ax B A C D) (@Cong Ax A B D C)) *)
assert (Cong A B D C) by (conclude lemma_congruencetransitive).
(* Goal: and (@Cong Ax B A D C) (and (@Cong Ax B A C D) (@Cong Ax A B D C)) *)
assert (Cong B A D C) by (conclude lemma_congruencetransitive).
(* Goal: and (@Cong Ax B A D C) (and (@Cong Ax B A C D) (@Cong Ax A B D C)) *)
close.
Qed.

End Euclid.


