proposition: Lemma inangle2__lea : forall A B C P Q, InAngle P A B C -> InAngle Q A B C -> LeA P B Q A B C.
proof: Proof. intros A B C P Q HP HQ. assert (HP' := l11_24 P A B C HP). assert (HQ' := l11_24 Q A B C HQ). assert (Hd := inangle_distincts A B C P HP); assert (Hd' := inangle_distincts A B C Q HQ); spliter; clean. destruct (col_dec A B C) as [HCol|HNCol]. { destruct (bet_dec A B C). apply l11_31_2; auto. apply l11_31_1; auto. assert (Out B A C) by (apply not_bet_out; assumption). apply l6_7 with A; [apply l6_6|]; apply in_angle_out with C; auto. } destruct (col_dec B P Q) as [HCol1|HNCol1]. apply l11_31_1; auto; apply col_inangle2__out with A C; auto. intro; apply HNCol; Col. destruct (col_dec B A P) as [HCol2|HNCol2]. { assert (Out B A P) by (apply col_in_angle_out with C; auto; intro; apply HNCol; Col). exists Q; split; trivial. apply out2__conga; [|apply out_trivial]; auto. } destruct (col_dec B C P) as [HCol3|HNCol3]. { assert (Out B C P). apply col_in_angle_out with A; auto; intro; apply HNCol; Col. apply lea_right_comm. exists Q; split; trivial. apply out2__conga; [|apply out_trivial]; auto. } destruct (col_dec B A Q) as [HCol4|HNCol4]. { assert (Out B A Q) by (apply col_in_angle_out with C; auto; intro; apply HNCol; Col). apply lea_left_comm. exists P; split; trivial. apply out2__conga; [|apply out_trivial]; auto. } destruct (col_dec B C Q) as [HCol5|HNCol5]. { assert (Out B C Q). apply col_in_angle_out with A; auto; intro; apply HNCol; Col. apply lea_comm. exists P; split; trivial. apply out2__conga; [|apply out_trivial]; auto. } destruct (cop__one_or_two_sides B P A Q) as [HOS|HTS]; Col. apply coplanar_perm_2, coplanar_trans_1 with C; Cop; Col. - apply lea_trans with P B C; [|apply lea_comm]; apply inangle__lea; trivial. apply os2__inangle; apply invert_one_side. exists A; split; Side; apply in_angle_two_sides; Col. apply one_side_transitivity with A; [|apply one_side_symmetry]; apply in_angle_one_side; Col. - apply lea_trans with A B P; [apply lea_right_comm|]; apply inangle__lea; trivial. apply os2__inangle; trivial. apply invert_one_side, one_side_transitivity with C; [|apply one_side_symmetry]; apply in_angle_one_side; Col. Qed.
imports: GeoCoq.Tarski_dev.Ch10_line_reflexivity_2