Require Export GeoCoq.Elements.OriginalProofs.lemma_8_2.
Require Export GeoCoq.Elements.OriginalProofs.lemma_8_3.

Section Euclid.
Context `{Ax:euclidean_neutral_ruler_compass}.
Lemma lemma_altitudebisectsbase : 
   forall A B M P, 
   BetS A M B -> Cong A P B P -> Per A M P ->
   Midpoint A M B.
Proof.
(* Goal: forall (A B M P : @Point Ax0) (_ : @BetS Ax0 A M B) (_ : @Cong Ax0 A P B P) (_ : @Per Ax0 A M P), @Midpoint Ax0 A M B *)
intros.
let Tf:=fresh in
assert (Tf:exists C, (BetS A M C /\ Cong A M C M /\ Cong A P C P /\ neq M P)) by (conclude_def Per );destruct Tf as [C];spliter.
(* Goal: @Midpoint Ax0 A M B *)
assert (BetS C M A) by (conclude axiom_betweennesssymmetry).
(* Goal: @Midpoint Ax0 A M B *)
assert (Cong C M A M) by (conclude lemma_congruencesymmetric).
(* Goal: @Midpoint Ax0 A M B *)
assert (Cong C P A P) by (conclude lemma_congruencesymmetric).
(* Goal: @Midpoint Ax0 A M B *)
assert (Per C M P) by (conclude_def Per ).
(* Goal: @Midpoint Ax0 A M B *)
assert (Per P M A) by (conclude lemma_8_2).
let Tf:=fresh in
assert (Tf:exists Q, (BetS P M Q /\ Cong P M Q M /\ Cong P A Q A /\ neq M A)) by (conclude_def Per );destruct Tf as [Q];spliter.
(* Goal: @Midpoint Ax0 A M B *)
assert (Cong Q M P M) by (conclude lemma_congruencesymmetric).
(* Goal: @Midpoint Ax0 A M B *)
assert (Per P M C) by (conclude lemma_8_2).
(* Goal: @Midpoint Ax0 A M B *)
assert (Out M C B) by (conclude_def Out ).
(* Goal: @Midpoint Ax0 A M B *)
assert (Per P M B) by (conclude lemma_8_3).
let Tf:=fresh in
assert (Tf:exists E, (BetS P M E /\ Cong P M E M /\ Cong P B E B /\ neq M B)) by (conclude_def Per );destruct Tf as [E];spliter.
(* Goal: @Midpoint Ax0 A M B *)
assert (Cong P A P B) by (forward_using lemma_congruenceflip).
(* Goal: @Midpoint Ax0 A M B *)
assert (Cong M Q P M) by (forward_using lemma_congruenceflip).
(* Goal: @Midpoint Ax0 A M B *)
assert (Cong P M M Q) by (conclude lemma_congruencesymmetric).
(* Goal: @Midpoint Ax0 A M B *)
assert (Cong E M P M) by (conclude lemma_congruencesymmetric).
(* Goal: @Midpoint Ax0 A M B *)
assert (Cong E M M Q) by (conclude lemma_congruencetransitive).
(* Goal: @Midpoint Ax0 A M B *)
assert (Cong M E M Q) by (forward_using lemma_congruenceflip).
(* Goal: @Midpoint Ax0 A M B *)
assert (Cong M Q M E) by (conclude lemma_congruencesymmetric).
(* Goal: @Midpoint Ax0 A M B *)
assert (neq P M) by (forward_using lemma_betweennotequal).
(* Goal: @Midpoint Ax0 A M B *)
assert (eq Q E) by (conclude lemma_extensionunique).
(* Goal: @Midpoint Ax0 A M B *)
assert (Cong P B Q B) by (conclude cn_equalitysub).
(* Goal: @Midpoint Ax0 A M B *)
assert (Cong A P P B) by (forward_using lemma_congruenceflip).
(* Goal: @Midpoint Ax0 A M B *)
assert (Cong A P Q B) by (conclude lemma_congruencetransitive).
(* Goal: @Midpoint Ax0 A M B *)
assert (Cong A Q A P) by (forward_using lemma_doublereverse).
(* Goal: @Midpoint Ax0 A M B *)
assert (Cong A Q Q B) by (conclude lemma_congruencetransitive).
(* Goal: @Midpoint Ax0 A M B *)
assert (Cong A Q B Q) by (forward_using lemma_congruenceflip).
(* Goal: @Midpoint Ax0 A M B *)
assert (Cong P Q P Q) by (conclude cn_congruencereflexive).
(* Goal: @Midpoint Ax0 A M B *)
assert (eq A A) by (conclude cn_equalityreflexive).
(* Goal: False *)
assert (eq B B) by (conclude cn_equalityreflexive).
(* Goal: @Midpoint Ax0 A M B *)
assert (nCol A M P) by (conclude lemma_rightangleNC).
(* Goal: @Midpoint Ax0 A M B *)
assert (~ Col A P M).
(* Goal: not (@neq Ax0 A P) *)
(* Goal: False *)
 {
(* Goal: not (@neq Ax0 A P) *)
 intro.
(* Goal: False *)
 assert (Col A M P) by (forward_using lemma_collinearorder).
(* Goal: False *)
 contradict.
 }
(* Goal: @Midpoint Ax0 A M B *)
assert (~ eq A P).
(* Goal: not (@neq Ax0 A P) *)
(* Goal: False *)
 {
(* Goal: not (@neq Ax0 A P) *)
 intro.
(* Goal: False *)
 assert (Col A P M) by (conclude_def Col ).
(* Goal: False *)
 contradict.
 }
(* Goal: @Midpoint Ax0 A M B *)
assert (neq P A) by (conclude lemma_inequalitysymmetric).
(* Goal: @Midpoint Ax0 A M B *)
assert (Out P A A) by (conclude lemma_ray4).
(* Goal: @Midpoint Ax0 A M B *)
assert (~ eq P B).
(* Goal: not (@neq Ax0 A P) *)
(* Goal: False *)
 {
(* Goal: not (@neq Ax0 A P) *)
 intro.
(* Goal: False *)
 assert (Cong A P B B) by (conclude cn_equalitysub).
(* Goal: False *)
 assert (~ neq A P).
(* Goal: not (@neq Ax0 A P) *)
(* Goal: False *)
  {
(* Goal: not (@neq Ax0 A P) *)
  intro.
(* Goal: False *)
  assert (neq B B) by (conclude axiom_nocollapse).
(* Goal: False *)
  assert (eq B B) by (conclude cn_equalityreflexive).
(* Goal: False *)
  contradict.
  }
(* Goal: False *)
 contradict.
 }
(* Goal: @Midpoint Ax0 A M B *)
assert (Out P B B) by (conclude lemma_ray4).
(* Goal: @Midpoint Ax0 A M B *)
assert (Out P M Q) by (conclude lemma_ray4).
(* Goal: @Midpoint Ax0 A M B *)
assert (CongA A P M B P M) by (conclude_def CongA ).
(* Goal: @Midpoint Ax0 A M B *)
assert (Cong P M P M) by (conclude cn_congruencereflexive).
(* Goal: @Midpoint Ax0 A M B *)
assert ((Cong A M B M /\ CongA P A M P B M /\ CongA P M A P M B)) by (conclude proposition_04).
(* Goal: @Midpoint Ax0 A M B *)
assert (Cong A M M B) by (forward_using lemma_congruenceflip).
(* Goal: @Midpoint Ax0 A M B *)
assert (Midpoint A M B) by (conclude_def Midpoint ).
(* Goal: @Midpoint Ax0 A M B *)
close.
Qed.

End Euclid.
