Library terre

Require Import Cring ssreflect ssrfun ssrbool eqtype ssrnat finset bigop.
Require Import seq choice fintype tuple div zmodp ssralg ssrnum.


Local Open Scope ring_scope.
Import GRing.Theory.

Section Terre.

(* Un corps quelconque                                                        *)
Variable R : fieldType.

(* Le nombre Pi                                                               *)

Variable Pi : R.

Hypothesis NZPi : Pi != 0.
Hypothesis NZP2 : 2%:R != 0 :> R.

Definition length (r : R) := 2%:R * Pi * r.

Definition delta := 1 / (2%:R * Pi).

Lemma delta_length r1 r2 k : length r1 - length r2 = k -> r1 = r2 + k * delta.

Fact result r1 r2 : length r1 - length r2 = 6%:R -> r1 = r2 + 3%:R / Pi.

End Terre.