proposition: Lemma prod_1_r : forall O E E' A, ~ Col O E E' -> Col O E A -> Prod O E E' A E A.
proof: Proof. intros. unfold Prod. repeat split; Col. exists E'. assert(HH:=(grid_not_par O E E' H)). spliter. repeat split. left. right. repeat split; Col. Col. left. assert(E' <> A). intro. subst A. contradiction. right. repeat split; Col. Qed.
imports: GeoCoq.Tarski_dev.Ch14_sum