proposition: Lemma grad_sum : forall A B C D E, Grad A B C -> Grad A B D -> Bet A C E -> Cong A D C E -> Grad A B E.
proof: Proof. intros A B C D E HGC HGD. elim (eq_dec_points A B). { intros; subst B. assert(A = C) by (apply grad112__eq; trivial). assert(A = D) by (apply grad112__eq; trivial). treat_equalities; trivial. } intro HAB. revert E. induction HGD. intro E; apply grad_stab; trivial. rename C0 into D; rename C' into D'. intros E' HBet' HCong'. destruct(segment_construction A C A D) as [E [HBet HCong]]. assert (HBet1 : Bet A B C) by (apply grad__bet; trivial). assert (HBet2 : Bet A B D) by (apply grad__bet; trivial). assert(HBet3 : Bet C E E'). { apply l6_13_1. assert_diffs; apply l6_2 with A; Between. apply (l5_6 A D A D'); Cong. apply bet__le1213; trivial. } apply grad_stab with E; auto with cong; eBetween. apply cong_transitivity with D D'; auto. apply l4_3_1 with A C; Cong. Qed.
imports: GeoCoq.Tarski_dev.Ch08_orthogonality Relations