proposition: Lemma prod_0_r : forall O E E' A, ~ Col O E E' -> Col O E A -> Prod O E E' A O O.
proof: Proof. intros. unfold Prod. repeat split; Col. exists O. repeat split; try (apply pj_trivial). Col. Qed.
imports: GeoCoq.Tarski_dev.Ch14_sum