proposition: Lemma grad_neq__neq12 : forall A B C, Grad A B C -> A <> C -> A <> B.
proof: Proof. intros A B C HG. elim HG; clear HG A B C; intros; intro; treat_equalities. auto. apply H0; auto. Qed.
imports: GeoCoq.Tarski_dev.Ch08_orthogonality Relations