proposition: Lemma cong_preserves_col : forall A B C A' B' C', BetH A B C -> CongH A B A' B' -> CongH B C B' C' -> CongH A C A' C' -> ColH A' B' C'.
proof: Proof. intros. induction(colH_dec A' B' C'). assumption. exfalso. apply betH_expand in H. spliter. assert(A' <> C'). { intro. subst C'. apply H3. Col. } assert(exists C0 : Point, CongH A' C0 A B /\ outH A' C' C0). apply(out_construction A' C' A B); auto. ex_and H9 B''. apply outH_expand in H10. spliter. apply outH_sym in H10; auto. assert(BetH A' B'' C'). { apply(betH_congH3_outH_betH A B C A' B'' C'); auto using congH_sym. } assert(A' <> B'). { intro. subst B'. apply H3;Col. } assert(exists E : Point, BetH A' B' E /\ CongH B' E B C). { apply(segment_constructionH A' B' B C); auto. } ex_and H16 C''. apply betH_expand in H14. apply betH_expand in H16. spliter. assert(CongH B C B'' C'). { apply(soustraction_betH A B C A' B'' C'); auto using congH_sym. } assert(CongH A' C'' A' C'). { apply(addition A' B' C'' A' B'' C'); auto. apply bet_disjoint; auto. apply bet_disjoint; auto. apply (cong_pseudo_transitivity A B); auto using congH_sym. apply (cong_pseudo_transitivity B C); auto using congH_sym. } assert(~ColH A' C'' C'). { intro. apply H3. apply (colH_trans A' C''); Col. } assert(CongaH A' C'' C' A' C' C''). { apply(isosceles_congaH A' C'' C'); auto. } assert(~ ColH B' C'' C'). { intro. apply H3. ColHR. } assert(CongaH B' C'' C' B' C' C''). { apply(isosceles_congaH B' C'' C'); auto. apply (cong_pseudo_transitivity B C); auto using congH_sym. } assert(CongaH A' C'' C' B' C'' C'). { apply(conga_out_conga B' C'' C' B' C'' C' A' C' B' C'). apply conga_refl. Col. left. Bet. right; right. split; auto. apply ncolH_expand in H30;intuition. right; right. split; auto. right; right. split; auto. apply ncolH_expand in H30;intuition. } assert(CongaH A' C' C'' B' C' C''). { apply(th19 C'' A' C' C' A' C'' C' B' C''); auto. intuition Col. intuition Col. intuition Col. apply(conga_out_conga B' C'' C' B' C' C'' A' C' B' C''); auto. left. Bet. right; right. split; auto. apply ncolH_expand in H30;intuition. right; right. split; auto. apply ncolH_expand in H30;intuition. right; right. split; auto. apply ncolH_expand in H30;intuition. } assert(outH C' A' B'). { apply(cong_4_uniqueness A' C' C'' C' B' C'' A' B'). intro. apply H30. Col. intro. apply H28. Col. apply congaH_commr; intuition Col. apply conga_refl. intuition Col. apply congaH_commr; intuition Col. assert(C' <> C''). { intro. subst C''. apply H30; Col. } line C' C'' l H34. eapply (out_same_side' C' C'' C'' B' A' l); auto. intro. apply H30. line_col B' C' C''. Col. left. Bet. apply same_side_prime_refl. intuition Col. } apply outH_col in H34. apply H3. Col. Qed.
imports: Setoid Coq.Classes.Morphisms Coq.Classes.Morphisms_Prop GeoCoq.Axioms.gupta_inspired_variant_axioms GeoCoq.Meta_theory.Models.gupta_inspired_to_tarski GeoCoq.Tactics.Coinc.tactics_axioms GeoCoq.Tactics.Coinc.ColR GeoCoq.Meta_theory.Dimension_axioms.upper_dim_3 GeoCoq.Meta_theory.Parallel_postulates.parallel_postulates GeoCoq.Axioms.hilbert_axioms