proposition: Lemma axiom_hcong_1_uniqueness : forall A B l M A' B' A'' B'', A <> B -> IncidentL M l -> IncidentL A' l -> IncidentL B' l -> IncidentL A'' l -> IncidentL B'' l -> Between_H A' M B' -> Cong M A' A B -> Cong M B' A B -> Between_H A'' M B'' -> Cong M A'' A B -> Cong M B'' A B -> (A' = A'' /\ B' = B'') \/ (A' = B'' /\ B' = A'').
proof: Proof. unfold Between_H. unfold IncidentL. intros. spliter. assert(A' <> M /\ A'' <> M /\ B' <> M /\ B'' <> M /\ A' <> B' /\ A'' <> B''). repeat split; intro; treat_equalities; tauto. spliter. induction(out_dec M A' A''). left. assert(A' = A''). apply (l6_11_uniqueness M A B A''); try assumption. apply out_trivial. assumption. split. assumption. subst A''. apply (l6_11_uniqueness M A B B''); try assumption. unfold Out. repeat split; try assumption. eapply l5_2. apply H18. assumption. assumption. apply out_trivial. assumption. right. apply not_out_bet in H23. assert(A' = B''). apply (l6_11_uniqueness M A B A'); try assumption. apply out_trivial. assumption. unfold Out. repeat split; try assumption. eapply l5_2. apply H18. assumption. apply between_symmetry. assumption. split. assumption. subst B''. apply (l6_11_uniqueness M A B B'); try assumption. apply out_trivial. assumption. unfold Out. repeat split; try assumption. eapply l5_2. apply H20. apply between_symmetry. assumption. assumption. eapply col3. apply (Cond l). Col. Col. Col. Qed.
imports: Morphisms GeoCoq.Axioms.hilbert_axioms GeoCoq.Axioms.parallel_postulates GeoCoq.Meta_theory.Parallel_postulates.tarski_playfair GeoCoq.Meta_theory.Parallel_postulates.SPP_ID GeoCoq.Meta_theory.Dimension_axioms.upper_dim_3 GeoCoq.Meta_theory.Parallel_postulates.parallel_postulates GeoCoq.Utils.triples