proposition: Lemma suma_preserves_ghalfa : forall A B C D E F X Y Z A' B' C' D' E' F' X' Y' Z', Acute X Y Z -> SumA A B C D E F X Y Z -> SumA A' B' C' D' E' F' X' Y' Z' -> gHalfA A B C A' B' C' -> gHalfA D E F D' E' F' -> gHalfA X Y Z X' Y' Z'.
proof: Proof. intros A B C D E F X Y Z A' B' C' D' E' F' X' Y' Z' HAcute HSuma HSuma'. rewrite 3 ghalfa_chara. intros [HAcute1 HSuma1] [HAcute2 HSuma2]. split; [apply HAcute|]. assert_diffs. destruct (ex_suma A' B' C' D E F) as [G [H [I]]]; auto. assert (SumA A B C X Y Z G H I) by (apply suma_assoc_1 with A B C D E F A' B' C'; SumA). apply suma_assoc_1 with A B C D E F G H I; [SumA..|]. apply suma_assoc_2 with A' B' C' D E F D' E' F'; [|SumA..]. apply sams_assoc_2 with A B C A B C X Y Z; SumA. Qed.
imports: GeoCoq.Tarski_dev.Annexes.suma