proposition: Lemma sum_par_strict : forall A B C A' C', Ar2 O E E' A B C -> A <> O -> Pj E E' A A' -> Col O E' A' -> Pj O E A' C' -> Pj O E' B C' -> Pj E' E C' C -> A' <> O /\ (Par_strict O E A' C' \/ B = O).
proof: Proof. intros. assert(Sum O E E' A B C). unfold Sum. split. auto. exists A'. exists C'. repeat split; auto. unfold Ar2 in H. unfold Pj in *. spliter. assert(A' <> O). intro. subst A'. induction H3. induction H3. apply H3. exists O. split; Col. spliter. induction H1. induction H1. apply H1. exists E. split; Col. spliter. apply grid_ok. apply(col_transitivity_1 _ A); Col. contradiction. subst C'. induction H1. induction H1. apply H1. exists E. split; Col. spliter. apply grid_ok. apply(col_transitivity_1 _ A); Col. contradiction. split. auto. induction(eq_dec_points B O). tauto. left. induction H3. induction H3. assumption. spliter. apply False_ind. apply grid_ok. assert(Col A' O E ). apply(col_transitivity_1 _ C'); Col. apply(col_transitivity_1 _ A'); Col. subst C'. apply False_ind. induction H4. induction H3. apply H3. exists A'. split; Col. spliter. assert(Col O B E'). apply (col_transitivity_1 _ A'); Col. apply grid_ok. apply (col_transitivity_1 _ B); Col. subst A'. assert(HH:= grid_not_par). spliter. induction H5. apply H3. apply par_symmetry. apply (par_col_par _ _ _ B); Col. apply par_right_comm. apply (par_col_par _ _ _ C); Par. apply col_permutation_1. apply(col_transitivity_1 _ E); Col. subst C. apply grid_ok. apply(col_transitivity_1 _ B); Col. Qed.
imports: GeoCoq.Tarski_dev.Ch13_6_Desargues_Hessenberg