proposition: Lemma opp_pythrel : forall O E E' A B C C' , Opp O E E' C C' -> PythRel O E E' A B C -> PythRel O E E' A B C'.
proof: Proof. intros. unfold PythRel in *. spliter. split. unfold Ar2 in *. spliter. repeat split; auto. unfold Opp in H. unfold Sum in H. spliter. unfold Ar2 in H. spliter. tauto. unfold Ar2 in H0. spliter. induction H1. left. spliter. induction H5. subst A. split. auto. right; auto. split. auto. subst B. left. unfold Opp in *. apply(sum_uniquenessA O0 E0 E'0 H0 C A C' O0); auto. apply sum_comm; auto. ex_and H1 B'. right. exists B'. repeat split; auto. apply opp_midpoint in H. unfold Midpoint in H. spliter. apply cong_transitivity with O0 C; Cong. Qed.
imports: Description Ring Field Nsatz Rtauto GeoCoq.Tarski_dev.Ch16_coordinates GeoCoq.Tarski_dev.Ch15_pyth_rel GeoCoq.Tarski_dev.Annexes.midpoint_theorems