proposition: Lemma reach__ex_gradexp_lt : forall A B P Q, A <> B -> Reach P Q A B -> exists C, GradExp A C B /\ Lt A C P Q.
proof: Proof. intros A B P Q HAB HReach. apply reach__ex_gradexp_le in HReach. destruct HReach as [R [HR1 HR2]]. generalize dependent B. induction HR1; rename A0 into P, B into Q; intros. { destruct (midpoint_existence A B) as [C []]. exists C; split. rewrite gradexp__gradexpinv. apply gradexpinv_stab with B; auto; constructor. apply le3456_lt__lt with A B; trivial. split; Le. intro; assert (C = B) by (apply (between_cong A); assumption). treat_equalities; auto. } rename C into R, C' into R'. destruct (midpoint_existence A B) as [M HM]. assert_diffs. destruct (IHHR1 M) as [C []]; auto. apply le_mid2__le12 with B R'; [|split|]; trivial. exists C; split; trivial. destruct HM. apply gradexp_stab with M; trivial. Qed.
imports: GeoCoq.Tarski_dev.Ch08_orthogonality Relations