proposition: Lemma in_angle_trans2 : forall A B C D E, InAngle C A B D -> InAngle D A B E -> InAngle D C B E.
proof: Proof. intros A B C D E HC HD. destruct (segment_construction E B E B) as [E' [HE1 HE2]]. assert (Hd := HD). apply inangle_distincts in Hd. spliter; assert_diffs. apply l11_24, in_angle_reverse with E'; Between. apply l11_24, in_angle_trans with A; apply l11_24; trivial. apply in_angle_reverse with E; auto. apply l11_24; trivial. Qed.
imports: GeoCoq.Tarski_dev.Ch10_line_reflexivity_2