proposition: Lemma reach__grad_min : forall A B C, A <> B -> Bet A B C -> Reach A B A C -> exists D E, Bet A D C /\ Grad A B D /\ E <> C /\ Bet A C E /\ Bet A D E /\ Cong A B D E.
proof: Proof. intros A B C HAB HBet HReach. destruct HReach as [D [HD1 HD2]]. apply l6_13_1 in HD2; [|apply l6_7 with B; [apply l6_6|]; apply bet_out; auto; apply grad__bet, HD1]. revert dependent C. induction HD1. intros; assert (B = C) by (apply between_equality with A; Between); subst C. destruct (segment_construction A B A B) as [C []]. assert_diffs. exists B, C; repeat split; Between; Cong; constructor. intros; destruct (l5_3 A C0 C C'); trivial. apply IHHD1; assumption. destruct (eq_dec_points C' C0). - subst C0. destruct (segment_construction A C' A B) as [C'' []]. assert_diffs. exists C', C''; repeat split; Cong. apply grad_stab with C; assumption. - exists C, C'; repeat split; assumption. Qed.
imports: GeoCoq.Tarski_dev.Ch08_orthogonality Relations