proposition: Lemma inangle_halfa2__inangle : forall O A B C A' C', ~ Col A O B -> InAngle C A O B -> HalfA A' A O B -> HalfA C' C O B -> InAngle C' A' O B.
proof: Proof. intros O A B C A' C' HNCol HC HA' HC'. apply halfa_sym in HA'. apply halfa_sym in HC'. destruct (col_dec B O C). { apply out341__inangle. apply halfa_distincts in HA'; spliter; auto. apply null_halfa__null with C; assumption. } apply l11_24, lea_in_angle. apply halfa2_lea__lea2 with A C; [assumption..|]. apply inangle__lea, l11_24, HC. apply one_side_transitivity with A; [|apply one_side_transitivity with C; apply one_side_symmetry]; apply in_angle_one_side; Col. apply halfa_not_null in HA'; Col. destruct HA' as [_ []]; assumption. apply l11_24, HC. apply halfa_not_null in HC'; Col. destruct HC' as [_ []]; Col. Qed.
imports: GeoCoq.Tarski_dev.Annexes.suma