proposition: Lemma reach__ex_gradexp_le : forall A B C D, Reach A B C D -> exists B', GradExp A B B' /\ Le C D A B'.
proof: Proof. intros A B C D HR. destruct HR as [B0 [HG HLe]]. destruct (grad__ex_gradexp_le A B B0 HG) as [B' [HG2 HLe2]]. exists B'; split; trivial. apply le_transitivity with A B0; trivial. Qed.
imports: GeoCoq.Tarski_dev.Ch08_orthogonality Relations