proposition: Lemma grid_not_par : ~Par O E E E' /\ ~Par O E O E' /\ ~Par O E' E E' /\ O <> E /\ O <> E' /\ E <> E'.
proof: Proof. repeat split. intro. unfold Par in H. induction H. apply H. exists E. split; Col. spliter. contradiction. intro. induction H. apply H. exists O. split; Col. spliter. apply grid_ok. Col. intro. induction H. apply H. exists E'. split; Col. spliter. contradiction. intro. subst E. apply grid_ok. Col. intro. subst E'. apply grid_ok. Col. intro. subst E'. apply grid_ok. Col. Qed.
imports: GeoCoq.Tarski_dev.Ch13_6_Desargues_Hessenberg