proposition: Lemma ghalfa2__conga_2 : 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'' [P' []] [P'' []]. apply conga_trans with A B P'; [assumption|]. apply conga_trans with A B P''; [|CongA]. apply out2__conga. apply out_trivial; assert_diffs; auto. apply halfa_uniqueness with A C; assumption. Qed.
imports: GeoCoq.Tarski_dev.Annexes.suma