proposition: Lemma cong_preserves_bet : forall A B C A' B' C', A'<>B' -> B'<>C' -> A'<>C' -> BetH A B C -> CongH A B A' B' -> CongH B C B' C' -> CongH A C A' C' -> BetH A' B' C'.
proof: Proof. intros A B C A' B' C' HD1 HD2 HD3 HBet1 HCong1 HCong2 HCong3. assert (HCol : ColH A' B' C'). { apply betH_expand in HBet1; spliter; apply cong_preserves_col_stronger with A B C; Col. } assert (HElim : outH A' B' C' \/ BetH B' A' C'). { apply between_one in HCol; auto; elim HCol; clear HCol; intro HCol; try (elim HCol; clear HCol; intro); auto; left; [left|right; left]; auto. apply between_comm; auto. } elim HElim; clear HElim; intro;[apply betH_congH3_outH_betH with A B C; auto|]. exfalso; apply betH_congH2__False with C B A C' B' A'; try apply between_comm; apply betH_expand in HBet1; spliter; auto using cong_permr, congH_perml. 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