Require Export GeoCoq.Elements.OriginalProofs.proposition_05.
Require Export GeoCoq.Elements.OriginalProofs.lemma_equalanglesNC.
Require Export GeoCoq.Elements.OriginalProofs.lemma_supplements.

Section Euclid.

Context `{Ax:euclidean_neutral_ruler_compass}.

Lemma proposition_05b : 
   forall A B C F G, 
   isosceles A B C -> BetS A B F -> BetS A C G ->
   CongA C B F B C G.
Proof.
(* Goal: forall (A B C F G : @Point Ax0) (_ : @isosceles Ax0 A B C) (_ : @BetS Ax0 A B F) (_ : @BetS Ax0 A C G), @CongA Ax0 C B F B C G *)
intros.
(* Goal: @CongA Ax0 C B F B C G *)
assert (CongA A B C A C B) by (conclude proposition_05).
(* Goal: @CongA Ax0 C B F B C G *)
assert (eq C C) by (conclude cn_equalityreflexive).
(* Goal: @CongA Ax0 C B F B C G *)
assert (nCol A C B) by (conclude lemma_equalanglesNC).
(* Goal: @CongA Ax0 C B F B C G *)
assert (~ eq B C).
(* Goal: not (@eq Ax0 B C) *)
(* Goal: @CongA Ax0 C B F B C G *)
 {
(* Goal: not (@eq Ax0 B C) *)
 intro.
(* Goal: False *)
 assert (Col A B C) by (conclude_def Col ).
(* Goal: False *)
 assert (Col A C B) by (forward_using lemma_collinearorder).
(* Goal: False *)
 contradict.
 }
(* Goal: @CongA Ax0 C B F B C G *)
assert (neq C B) by (conclude lemma_inequalitysymmetric).
(* Goal: @CongA Ax0 C B F B C G *)
assert (Out B C C) by (conclude lemma_ray4).
(* Goal: @CongA Ax0 C B F B C G *)
assert (Supp A B C C F) by (conclude_def Supp ).
(* Goal: @CongA Ax0 C B F B C G *)
assert (eq B B) by (conclude cn_equalityreflexive).
(* Goal: @CongA Ax0 C B F B C G *)
assert (Out C B B) by (conclude lemma_ray4).
(* Goal: @CongA Ax0 C B F B C G *)
assert (Supp A C B B G) by (conclude_def Supp ).
(* Goal: @CongA Ax0 C B F B C G *)
assert (CongA C B F B C G) by (conclude lemma_supplements).
(* Goal: @CongA Ax0 C B F B C G *)
close.
Qed.

End Euclid.


