proposition: Lemma compatibility_of_sum_with_order : forall O E E' A B C APC BPC, LeP O E E' A B -> Sum O E E' A C APC -> Sum O E E' B C BPC -> LeP O E E' APC BPC.
proof: Proof. intros O E E' A B C APC BPC HLe HAPC HBPC. elim HLe; clear HLe; intro HLe. { left; destruct HLe as [D [HDiff HPs]]; exists D; split; auto. assert (HNC : ~ Col O E E') by (apply diff_ar2 in HDiff; unfold Ar2 in *; spliter; Col). apply sum_diff; apply diff_sum in HDiff; apply sum_assoc_1 with C A B; auto; apply sum_comm; auto. } { treat_equalities. assert (APC = BPC) by (apply sum_uniqueness with O E E' A C; auto). treat_equalities; apply leP_refl. } Qed.
imports: GeoCoq.Tarski_dev.Ch14_prod