diff options
| author |  desmettr <desmettr@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2002-07-02 10:47:22 +0000 |
|---|---|---|
| committer | desmettr <desmettr@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2002-07-02 10:47:22 +0000 |
| commit | b2cf417b63a00f3a4944edf59f6e11aecf19fd01 (patch) | |
| tree | a274c18e30414054a828748ff210fe57901477b9 /theories/Reals/Rtrigo.v | |
| parent | 7cf6823fd4b9a20c1f84bc9f67cc43017f624dfc (diff) | |
Suppression de l'axiome arc_sin_cos
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2823 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/Reals/Rtrigo.v')
| -rw-r--r-- | theories/Reals/Rtrigo.v | 6 |
1 files changed, 0 insertions, 6 deletions
diff --git a/theories/Reals/Rtrigo.v b/theories/Reals/Rtrigo.v index eb89ef801..6dcd087a8 100644 --- a/theories/Reals/Rtrigo.v +++ b/theories/Reals/Rtrigo.v @@ -69,12 +69,6 @@ Intro x; Generalize (cos2 x); Intro H1; Rewrite -> H1. Unfold Rminus; Rewrite Ropp_distr1; Rewrite <- Rplus_assoc; Rewrite Rplus_Ropp_r; Rewrite Rplus_Ol; Symmetry; Apply Ropp_Ropp. Qed. -Axiom arc_sin_cos : (x,y,z:R) ``0<=x`` -> ``0<=y`` -> ``0<=z`` -> ``(Rsqr x)+(Rsqr y)==(Rsqr z)`` -> (EXT t : R | (x==(Rmult z (cos t))) /\ (y==(Rmult z (sin t)))). - -Lemma pythagorean : (x,y,z:R) ``(Rsqr x)+(Rsqr y)==(Rsqr z)`` -> ``0<=x`` -> ``0<=y`` -> ``0<=z`` -> (EXT t : R | z==(Rplus (Rmult x (cos t)) (Rmult y (sin t)))). -Intros x y z H1 H2 H3 H4; Generalize (arc_sin_cos x y z H2 H3 H4); Intro H5; Elim H5; [ Intros x0 H6; Elim H6; Intros H7 H8; Exists x0; Rewrite H7; Rewrite H8; Replace ``z*(cos x0)*(cos x0)+z*(sin x0)*(sin x0)`` with ``z*((Rsqr (sin x0))+(Rsqr (cos x0)))``; [ Rewrite sin2_cos2; Ring | Unfold Rsqr; Ring] | Assumption]. -Qed. - Lemma aze : ``2<>0``. DiscrR. Qed. |