proposition: Lemma prodp_to_prod : forall O E E' A B C, Prodp O E E' A B C -> Prod O E E' A B C.
proof: Proof. intros. unfold Prodp in H. spliter. ex_and H1 B'. unfold Prod. split. unfold Ar2. unfold Proj in *. spliter. repeat split; Col. intro. apply H8. right. repeat split; Col. exists B'. repeat split. eapply (project_pj _ _ O E'); auto. unfold Proj in H1. tauto. eapply (project_pj _ _ O E); auto. unfold Proj. unfold Proj in H2. spliter. repeat split; Col. intro. induction H7. apply H7. exists A. split; Col. spliter. apply H4. right. repeat split; Col. induction H6. left. apply par_right_comm. auto. right. auto; intro. Qed.
imports: GeoCoq.Tarski_dev.Ch14_sum