proposition: Lemma prod_to_prodp : forall O E E' A B C, Prod O E E' A B C -> Prodp O E E' A B C.
proof: Proof. intros. unfold Prod in H. spliter. unfold Prodp. ex_and H0 B'. unfold Ar2 in H. spliter. assert(O <> E' /\ E <> E'). split; intro; apply H; subst E'; Col. repeat split; try Col. exists B'. spliter. split. apply(pj_col_project B B' O E' E E'); Col. intro. induction H8. apply H8. exists E'. split; Col. apply H. tauto. apply(pj_col_project B' C O E A E'); Col. intro. subst E. apply H; Col. intro. subst E'. contradiction. intro. induction(eq_dec_points O A). subst A. induction H8. apply H8. exists O. split; Col. spliter. apply H. Col. induction H8. apply H8. exists A. split; Col. spliter. apply H. apply (col_transitivity_1 _ A); Col. unfold Pj in *. induction H2. left. apply par_left_comm. assumption. right; auto. Qed.
imports: GeoCoq.Tarski_dev.Ch14_sum