proposition: Lemma ghalfa2__conga_1 : forall A B C A' B' C' A'' B'' C'', gHalfA A B C A' B' C' -> gHalfA A B C A'' B'' C'' -> CongA A' B' C' A'' B'' C''.
proof: Proof. intros A B C A' B' C' A'' B'' C''. rewrite 2 ghalfa_chara. intros [HAcute' HSuma'] [HAcute'' HSuma'']. apply (suma2__conga A B C A B C); assumption. Qed.
imports: GeoCoq.Tarski_dev.Annexes.suma