proposition: Lemma sums__le1256 : forall A B C D E F, SumS A B C D E F -> Le A B E F.
proof: Proof. intros A B C D E F HSumS. destruct HSumS as [P [Q [R [HBet [HCong1 [HCong2 HCong3]]]]]]. apply (l5_6 P Q P R); trivial. exists Q; Cong. Qed.
imports: GeoCoq.Tarski_dev.Ch06_out_lines