proposition: Lemma diff_2_prod : forall O E E' A B AMB BMA ME, Opp O E E' E ME -> Diff O E E' A B AMB -> Diff O E E' B A BMA -> Prod O E E' AMB ME BMA.
proof: Proof. intros O E E' A B AMB BMA ME HOpp HAMB HBMA. apply opp_prod; auto; apply diff_opp with A B; auto. Qed.
imports: GeoCoq.Tarski_dev.Ch14_sum