1
(************************************************************************)
2
(* v * The Coq Proof Assistant / The Coq Development Team *)
3
(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
4
(* \VV/ **************************************************************)
5
(* // * This file is distributed under the terms of the *)
6
(* * GNU Lesser General Public License Version 2.1 *)
7
(************************************************************************)
9
(*i $Id: LegacyRfield.v 10739 2008-04-01 14:45:20Z herbelin $ i*)
11
Require Export Raxioms.
12
Require Export LegacyField.
13
Import LegacyRing_theory.
19
Lemma RLegacyTheory : Ring_Theory Rplus Rmult 1 0 Ropp (fun x y:R => false).
22
symmetry in |- *; apply Rplus_assoc.
24
symmetry in |- *; apply Rmult_assoc.
25
intro; apply Rplus_0_l.
26
intro; apply Rmult_1_l.
30
rewrite (Rmult_comm n p).
31
rewrite (Rmult_comm m p).
32
apply Rmult_plus_distr_l.
33
intros; contradiction.
39
R Rplus Rmult 1%R 0%R Ropp (fun x y:R => false) Rinv RLegacyTheory Rinv_l
40
with minus := Rminus div := Rdiv.