proposition: Lemma grad__ex_gradexp_le : forall A B C, Grad A B C -> exists D, GradExp A B D /\ Le A C A D.
proof: Proof. intros A B C. induction 1. exists B; split; Le; apply gradexp_init. destruct IHGrad as [D [HGE HLe]]. destruct (segment_construction A D A D) as [D' [HBet HCong]]. exists D'; split. apply gradexp_stab with D; Cong. apply bet2_le2__le1346 with C D; Le. apply gradexp__grad, grad__bet in HGE. apply l5_6 with A B A D; Cong; Le. Qed.
imports: GeoCoq.Tarski_dev.Ch08_orthogonality Relations