proposition: Lemma grad2__grad123 : forall A B C D E F, Grad2 A B C D E F -> Grad A B C.
proof: Proof. intros A B C D E F. induction 1. apply grad_init. apply (grad_stab _ _ C); auto. Qed.
imports: GeoCoq.Tarski_dev.Ch08_orthogonality Relations