proposition: Lemma prod_null : forall O E E' A B, Prod O E E' A B O -> A = O \/ B = O.
proof: Proof. intros. unfold Prod in H. spliter. ex_and H0 B'. induction(eq_dec_points B O). right. assumption. left. unfold Ar2 in H. spliter. unfold Pj in *. induction H0; induction H2. induction H2. apply False_ind. apply H2. exists E'. split; Col. spliter. apply(l6_21 O E B' O); Col. intro. apply H. ColR. subst B'. induction H0. apply False_ind. apply H0. exists E. split; Col. spliter. apply False_ind. apply H3. apply (l6_21 O E E' O); Col. intro. subst E'. apply H. Col. subst B'. induction H2. apply False_ind. apply H0. exists A. split; Col. apply (col3 O E); Col. intro. subst E. apply H; Col. spliter. apply False_ind. apply H2. apply (l6_21 O E E' O); Col. intro. subst E'. apply H. Col. subst B'. contradiction. Qed.
imports: GeoCoq.Tarski_dev.Ch14_sum