proposition: Lemma gradexp2__gradexp123 : forall A B C D E F, GradExp2 A B C D E F -> GradExp A B C.
proof: Proof. intros A B C D E F. induction 1. apply gradexp_init. apply (gradexp_stab _ _ C); auto. Qed.
imports: GeoCoq.Tarski_dev.Ch08_orthogonality Relations