proposition: Lemma prod_assoc : forall O E E' A B C AB BC ABC, Prod O E E' A B AB -> Prod O E E' B C BC -> (Prod O E E' A BC ABC <-> Prod O E E' AB C ABC).
proof: Proof. intros. split. intro. apply (prod_assoc1 O E E' A B _ _ BC); auto. intro. eapply (prod_assoc2 O E E' A B C AB ); auto. Qed.
imports: GeoCoq.Tarski_dev.Ch14_sum