proposition: Lemma distr_l_diff : forall O E E' A B C BMC AB AC ABMC, Diff O E E' B C BMC -> Prod O E E' A B AB -> Prod O E E' A C AC -> Prod O E E' A BMC ABMC -> Diff O E E' AB AC ABMC.
proof: Proof. intros O E E' A B C BMC AB AC ABMC HBMC HAB HAC HABMC. apply diff_sum in HBMC; apply sum_diff. apply distr_l with A C BMC B; auto. Qed.
imports: GeoCoq.Tarski_dev.Ch14_sum