proposition: Lemma leP_sum_leP : forall O E E' A B C X Y Z, LeP O E E' A X -> LeP O E E' B Y -> Sum O E E' A B C -> Sum O E E' X Y Z -> LeP O E E' C Z.
proof: Proof. intros. unfold LeP in *. assert(Ar2 O E E' A B C). apply sum_ar2; auto. assert(Ar2 O E E' X Y Z). apply sum_ar2; auto. unfold Ar2 in *. spliter. clean_duplicated_hyps. induction H; induction H0. unfold LtP in *. ex_and H dXA. ex_and H0 dYB. assert(HH:= diff_exists O E E' Z C H3 H7 H10). ex_and HH dZC. left. exists dZC. split; auto. assert(Sum O E E' dXA dYB dZC). apply(sum_diff2_diff_sum2_b O E E' A B C X Y Z dXA dYB dZC H1 H2 H H0); auto. apply(sum_pos_pos O E E' dXA dYB); auto. subst Y. left. unfold LtP in *. ex_and H dXA. assert(HH:=diff_exists O E E' Z C H3 H7 H10). ex_and HH dZC. exists dZC. split; auto. assert(Sum O E E' dXA O dZC). apply(sum_diff2_diff_sum2_b O E E' A B C X B Z dXA O dZC); auto. apply diff_null; auto. assert(dXA = dZC). apply(sum_A_O_eq O E E'); auto. subst dXA. assumption. subst X. left. unfold LtP in *. ex_and H0 dYB. assert(HH:=diff_exists O E E' Z C H3 H7 H10). ex_and HH dZC. exists dZC. split; auto. assert(Sum O E E' O dYB dZC). apply(sum_diff2_diff_sum2_b O E E' A B C A Y Z O dYB dZC); auto. apply diff_null; auto. assert(dYB = dZC). apply(sum_O_B_eq O E E'); auto. subst dYB. assumption. subst X. subst Y. right. apply(sum_uniqueness O E E' A B); auto. Qed.
imports: GeoCoq.Tarski_dev.Ch14_prod