proposition: Lemma ghalfa_preserves_conga_2 : forall A B C A' B' C' X Y Z X' Y' Z', gHalfA X Y Z A B C -> gHalfA X' Y' Z' A' B' C' -> CongA A B C A' B' C' -> CongA X Y Z X' Y' Z'.
proof: Proof. intros A B C A' B' C' X Y Z X' Y' Z' [P []] [P' []] HConga. apply conga_trans with A B P. assumption. apply conga_trans with A' B' P'; [|apply conga_sym; assumption]. apply conga_halfa__conga2 with C C'; assumption. Qed.
imports: GeoCoq.Tarski_dev.Annexes.suma