proposition: Lemma grad112__eq : forall A B, Grad A A B -> A = B.
proof: Proof. intros A B HG. assert (HA' : exists A', A' = A /\ Grad A A' B) by (exists A; auto). destruct HA' as [A' [Heq HG']]. clear HG. revert Heq. elim HG'; auto. clear HG' A B A'. intros; treat_equalities; auto. Qed.
imports: GeoCoq.Tarski_dev.Ch08_orthogonality Relations