proposition: Lemma th19: forall O A B O1 A1 B1 O2 A2 B2, ~ ColH O A B -> ~ ColH O1 A1 B1 -> ~ ColH O2 A2 B2 -> CongaH A O B A1 O1 B1 -> CongaH A O B A2 O2 B2 -> CongaH A1 O1 B1 A2 O2 B2.
proof: Proof. intros. assert (T1:=ncolH_distincts O A B H). assert (T2:=ncolH_distincts O1 A1 B1 H0). assert (T3:=ncolH_distincts O2 A2 B2 H1). spliter. elim (out_construction O1 A1 O A);auto. intros A1' [T1 T2]. elim (out_construction O2 A2 O A);auto. intros A2' [T3 T4]. elim (out_construction O1 B1 O B);auto. intros B1' [T5 T6]. elim (out_construction O2 B2 O B);auto. intros B2' [T7 T8]. assert (T2' := T2). apply outH_expand in T2'. assert (T4' := T4). apply outH_expand in T4'. assert (T6':=T6). apply outH_expand in T6'. spliter. assert (T8':=T8). apply outH_expand in T8'. spliter. assert (CongH A B A1' B1'). { apply (th12 O A B O1 A1' B1' ). intro;apply H;Col. intro;apply H0;ColHR. apply congH_perms in T1;spliter;auto. apply congH_perms in T5;spliter;auto. apply conga_out_conga with A B A1 B1;auto using outH_trivial. } assert (CongH A B A2' B2'). { apply (th12 O A B O2 A2' B2' ). intro;apply H;Col. intro;apply H1;ColHR. apply congH_perms in T3;spliter;auto. apply congH_perms in T7;spliter;auto. apply conga_out_conga with A B A2 B2;auto using outH_trivial. } assert (CongH A1' B1' A2' B2') by (apply cong_pseudo_transitivity with A B;auto). assert (CongaH A1' O1 B1' A2' O2 B2'). { apply (th18_aux O1 A1' B1' O2 A2' B2'). intro;apply H0;ColHR. intro;apply H1;ColHR. apply cong_pseudo_transitivity with O A. apply congH_perms in T1;spliter;auto. apply congH_perms in T3;spliter;auto. apply cong_pseudo_transitivity with O B. apply congH_perms in T5;spliter;auto. apply congH_perms in T7;spliter;auto. assumption. } apply conga_out_conga with A1' B1' A2' B2';auto using outH_trivial, outH_sym. 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