proposition: Lemma per_cong_mid : forall A B C H, B <> C -> Bet A B C -> Cong A H C H -> Per H B C -> Midpoint B A C.
proof: Proof. intros. induction (eq_dec_points H B). subst H. unfold Midpoint. split. assumption. apply cong_right_commutativity. assumption. assert(Per C B H). apply l8_2. assumption. assert (Per H B A). eapply per_col. apply H0. assumption. unfold Col. right; right. assumption. assert (Per A B H). apply l8_2. assumption. unfold Per in *. ex_and H3 C'. ex_and H5 H'. ex_and H6 A'. ex_and H7 H''. assert (H' = H''). eapply (construction_uniqueness H B H B). assumption. apply midpoint_bet. assumption. apply cong_commutativity. apply midpoint_cong. apply l7_2. apply H5. apply midpoint_bet. assumption. apply cong_commutativity. apply midpoint_cong. apply l7_2. assumption. subst H''. assert(IFSC H B H' A H B H' C). repeat split. apply midpoint_bet. assumption. apply midpoint_bet. assumption. apply cong_reflexivity. apply cong_reflexivity. apply cong_commutativity. assumption. apply cong_commutativity. eapply cong_transitivity. apply cong_symmetry. apply H11. eapply cong_transitivity. apply H2. assumption. eapply l4_2 in H12. unfold Midpoint. split. assumption. apply cong_left_commutativity. assumption. Qed.
imports: GeoCoq.Tarski_dev.Ch07_midpoint GeoCoq.Tactics.Coinc.ColR