proposition: Lemma distr_r : forall O E E' A B C D AC BC DC, Sum O E E' A B D -> Prod O E E' A C AC -> Prod O E E' B C BC -> (Prod O E E' D C DC -> Sum O E E' AC BC DC).
proof: Proof. intros. apply prod_comm in H0. apply prod_comm in H1. apply prod_comm in H2. apply(distr_l O E E' C A B D AC BC DC); auto. Qed.
imports: GeoCoq.Tarski_dev.Ch14_sum