proposition: Lemma cong_mid__suma : forall A B C M, ~ Col A B C -> Midpoint M A B -> Cong M A M C -> SumA C A B A B C A C B.
proof: Proof. intros A B C M HNCol HM HCong. assert_diffs. assert(CongA A B C M C B). { apply (l11_10 M B C M C B); Out. apply l11_44_1_a; auto; apply (cong_transitivity _ _ M A); Cong. } assert(CongA B A C M C A). { apply (l11_10 M A C M C A); Out. apply l11_44_1_a; Cong. } apply (conga3_suma__suma A C M M C B A C B); CongA. assert (TS M C A B) by (apply bet__ts; Between; intro; apply HNCol; ColR). exists B. repeat (split; CongA); Side; Cop. Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel GeoCoq.Tarski_dev.Annexes.suma