proposition: Lemma sum_assoc : forall O E E' A B C AB BC ABC, Sum O E E' A B AB -> Sum O E E' B C BC -> (Sum O E E' A BC ABC <-> Sum O E E' AB C ABC).
proof: Proof. intros. split; intro. apply(sum_assoc_1 O E E' A B C AB BC ABC); auto. apply(sum_assoc_2 O E E' A B C AB BC ABC); auto. Qed.
imports: GeoCoq.Tarski_dev.Ch13_6_Desargues_Hessenberg