proposition: Lemma bet_cong__ghalfa : forall A B C B', A <> B -> B <> C -> A <> B' -> Bet B A B' -> Cong A B A C -> gHalfA A B C C A B'.
proof: Proof. intros A B C B' HAB HBC HAB' HBet HCong. apply ghalfa_chara; split. apply cong__acute; auto. suma.assert_diffs. apply (conga3_suma__suma A B C B C A C A B'); try apply conga_refl; auto. apply high_school_exterior_angle_theorem; auto. apply conga_left_comm, l11_44_1_a; Cong. Qed.
imports: GeoCoq.Tarski_dev.Annexes.circles GeoCoq.Tarski_dev.Annexes.half_angles GeoCoq.Tarski_dev.Ch12_parallel_inter_dec