proposition: Lemma ghalfa_preserves_lta : forall A B C X Y Z A' B' C' X' Y' Z', gHalfA A' B' C' A B C -> gHalfA X' Y' Z' X Y Z -> LtA A B C X Y Z -> LtA A' B' C' X' Y' Z'.
proof: Proof. intros A B C X Y Z A' B' C' X' Y' Z' [P1 []] [P2 []] HLta. apply (conga_preserves_lta A B P1 X Y P2); [CongA..|]. apply halfa2_lta__lta2 with Z C; assumption. Qed.
imports: GeoCoq.Tarski_dev.Annexes.suma