proposition: Lemma opp0 : Opp O E E' O O.
proof: Proof. assert(NC:=grid_ok). assert(O <> E' /\ E <> E'). split; intro ; subst E'; apply NC; Col. spliter. assert(O <> E). intro. subst E. apply NC; Col. unfold Opp. apply sump_to_sum. unfold Sump. repeat split; Col. exists O. exists O. exists E. split. apply project_trivial; Col. intro. induction H2. apply H2. exists E'. split; Col. spliter. contradiction. split. apply par_reflexivity; auto. split. apply project_trivial; Col. intro. induction H2. apply H2. exists O. split; Col. spliter. apply NC. Col. apply project_trivial; Col. intro. induction H2. apply H2. exists E. split; Col. spliter. contradiction. Qed.
imports: GeoCoq.Tarski_dev.Ch13_6_Desargues_Hessenberg