proposition: Lemma grad_neq__neq13 : forall A B C, Grad A B C -> A <> B -> A <> C.
proof: Proof. intros A B C HG HAB Heq. subst C. apply HAB. apply between_identity, grad__bet; trivial. Qed.
imports: GeoCoq.Tarski_dev.Ch08_orthogonality Relations