proposition: Lemma gradexp_le__reach : forall A B C D B', GradExp A B B' -> Le C D A B' -> Reach A B C D.
proof: Proof. intros A B C D B' HGE HLe. exists B'; split; trivial. apply gradexp__grad; trivial. Qed.
imports: GeoCoq.Tarski_dev.Ch08_orthogonality Relations