(* mathcomp analysis (c) 2017 Inria and AIST. License: CeCILL-C.              *)
From Coq Require Import ssreflect ssrfun ssrbool.
From mathcomp Require Import ssrnat eqtype choice order ssralg ssrnum ssrint.
Notation "_ + _" was already used in scope nat_scope.
[notation-overridden,parsing]
Notation "_ - _" was already used in scope nat_scope.
[notation-overridden,parsing]
Notation "_ <= _" was already used in scope nat_scope.
[notation-overridden,parsing]
Notation "_ < _" was already used in scope nat_scope.
[notation-overridden,parsing]
Notation "_ >= _" was already used in scope nat_scope.
[notation-overridden,parsing]
Notation "_ > _" was already used in scope nat_scope.
[notation-overridden,parsing]
Notation "_ <= _ <= _" was already used in scope
nat_scope. [notation-overridden,parsing]
Notation "_ < _ <= _" was already used in scope
nat_scope. [notation-overridden,parsing]
Notation "_ <= _ < _" was already used in scope
nat_scope. [notation-overridden,parsing]
Notation "_ < _ < _" was already used in scope
nat_scope. [notation-overridden,parsing]
Notation "_ * _" was already used in scope nat_scope.
[notation-overridden,parsing]
New coercion path [GRing.subring_closedM;
                   GRing.smulr_closedN] : GRing.subring_closed >-> GRing.oppr_closed is ambiguous with existing 
[GRing.subring_closedB; GRing.zmod_closedN] : GRing.subring_closed >-> GRing.oppr_closed.
[ambiguous-paths,typechecker]
New coercion path [GRing.subring_closed_semi;
                   GRing.semiring_closedM] : GRing.subring_closed >-> GRing.mulr_closed is ambiguous with existing 
[GRing.subring_closedM; GRing.smulr_closedM] : GRing.subring_closed >-> GRing.mulr_closed.
New coercion path [GRing.subring_closed_semi;
                   GRing.semiring_closedD] : GRing.subring_closed >-> GRing.addr_closed is ambiguous with existing 
[GRing.subring_closedB; GRing.zmod_closedD] : GRing.subring_closed >-> GRing.addr_closed.
[ambiguous-paths,typechecker]
New coercion path [GRing.sdivr_closed_div;
                   GRing.divr_closedM] : GRing.sdivr_closed >-> GRing.mulr_closed is ambiguous with existing 
[GRing.sdivr_closedM; GRing.smulr_closedM] : GRing.sdivr_closed >-> GRing.mulr_closed.
[ambiguous-paths,typechecker]
New coercion path [GRing.subalg_closedBM;
                   GRing.subring_closedB] : GRing.subalg_closed >-> GRing.zmod_closed is ambiguous with existing 
[GRing.subalg_closedZ; GRing.submod_closedB] : GRing.subalg_closed >-> GRing.zmod_closed.
[ambiguous-paths,typechecker]
New coercion path [GRing.divring_closed_div;
                   GRing.sdivr_closedM] : GRing.divring_closed >-> GRing.smulr_closed is ambiguous with existing 
[GRing.divring_closedBM; GRing.subring_closedM] : GRing.divring_closed >-> GRing.smulr_closed.
[ambiguous-paths,typechecker]
New coercion path [GRing.divalg_closedBdiv;
                   GRing.divring_closedBM] : GRing.divalg_closed >-> GRing.subring_closed is ambiguous with existing 
[GRing.divalg_closedZ; GRing.subalg_closedBM] : GRing.divalg_closed >-> GRing.subring_closed.
[ambiguous-paths,typechecker]
New coercion path [GRing.Pred.subring_smul;
                   GRing.Pred.smul_mul] : GRing.Pred.subring >-> GRing.Pred.mul is ambiguous with existing 
[GRing.Pred.subring_semi; GRing.Pred.semiring_mul] : GRing.Pred.subring >-> GRing.Pred.mul.
[ambiguous-paths,typechecker]
From mathcomp.classical Require Import mathcomp_extra.
Notation "_ \* _" was already used in scope
ring_scope. [notation-overridden,parsing]
Notation "\- _" was already used in scope ring_scope.
[notation-overridden,parsing]

(******************************************************************************)
(* This file develops tools to make the manipulation of numbers with a known  *)
(* sign easier, thanks to canonical structures. This adds types like          *)
(* {posnum R} for positive values in R, a notation e%:pos that infers the     *)
(* positivity of expression e according to existing canonical instances and   *)
(* %:num to cast back from type {posnum R} to R.                              *)
(* For instance, given x, y : {posnum R}, we have                             *)
(* ((x%:num + y%:num) / 2)%:pos : {posnum R} automatically inferred.          *)
(*                                                                            *)
(* * types for values with known sign                                         *)
(*    {posnum R} == interface type for elements in R that are positive; R     *)
(*                  must have a zmodType structure.                           *)
(*                  Allows to solve automatically goals of the form x > 0 if  *)
(*                  x is canonically a {posnum R}. {posnum R} is canonically  *)
(*                  stable by common operations. All positive natural numbers *)
(*                  ((n.+1)%:R) are also canonically in {posnum R}            *)
(*    {nonneg R} == interface types for elements in R that are non-negative;  *)
(*                  R must have a zmodType structure. Automatically solves    *)
(*                  goals of the form x >= 0. {nonneg R} is stable by         *)
(*                  common operations. All natural numbers n%:R are also      *)
(*                  canonically in {nonneg R}.                                *)
(* {compare x0 & nz & cond} == more generic type of values comparing to       *)
(*                  x0 : T according to nz and cond (see below). T must have  *)
(*                  a porderType structure. This type is shown to be a        *)
(*                  porderType. It is also an orderTpe, as soon as T is a     *)
(*                  numDomainType.                                            *)
(* {num R & nz & cond} == {compare 0%R : R & nz & cond}. T must have a        *)
(*                  zmodType structure.                                       *)
(*        {= x0} == {compare x0 & ?=0 & =0}                                   *)
(*    {= x0 : T} == same with an explicit type T                              *)
(*        {> x0} == {compare x0 & !=0 & >=0}                                  *)
(*    {> x0 : T} == same with an explicit type T                              *)
(*        {< x0} == {compare x0 & !=0 & <=0}                                  *)
(*    {< x0 : T} == same with an explicit type T                              *)
(*       {>= x0} == {compare x0 & ?=0 & >=0}                                  *)
(*   {>= x0 : T} == same with an explicit type T                              *)
(*       {<= x0} == {compare x0 & ?=0 & <=0}                                  *)
(*   {<= x0 : T} == same with an explicit type T                              *)
(*      {>=< x0} == {compare x0 & ?=0 & >=<0}                                 *)
(*  {>=< x0 : T} == same with an explicit type T                              *)
(*       {>< x0} == {compare x0 & !=0 & >=<0}                                 *)
(*   {>< x0 : T} == same with an explicit type T                              *)
(*       {!= x0} == {compare x0 & !=0 & >?<0}                                 *)
(*   {!= x0 : T} == same with an explicit type T                              *)
(*       {?= x0} == {compare x0 & ?=0 & >?<0}                                 *)
(*   {?= x0 : T} == same with an explicit type T                              *)
(*                                                                            *)
(* * casts from/to values with known sign                                     *)
(*        x%:pos == explicitly casts x to {posnum R}, triggers the inference  *)
(*                  of a {posnum R} structure for x.                          *)
(*        x%:nng == explicitly casts x to {nonneg R}, triggers the inference  *)
(*                  of a {nonneg R} structure for x.                          *)
(*        x%:sgn == explicitly casts x to the most precise known              *)
(*                  {compare x0 & nz & cond} according to existing canonical  *)
(*                  instances.                                                *)
(*        x%:num == explicit cast from {compare x0 & nz & cond} to R. In      *)
(*                  particular this works from {posnum R} and {nonneg R} to R.*)
(*     x%:posnum == explicit cast from {posnum R} to R.                       *)
(*     x%:nngnum == explicit cast from {nonneg R} to R.                       *)
(*                                                                            *)
(* * nullity conditions nz                                                    *)
(* All nz above can be the following (in scope snum_nullity_scope delimited   *)
(* by %snum_nullity)                                                          *)
(*           !=0 == to encode x != 0                                          *)
(*           ?=0 == unknown nullity                                           *)
(*                                                                            *)
(* * reality conditions cond                                                  *)
(* All cond above can be the following (in scope snum_sign_scope delimited by *)
(* by %snum_sign)                                                             *)
(*            =0 == to encode x == 0                                          *)
(*           >=0 == to encode x >= 0                                          *)
(*           <=0 == to encode x <= 0                                          *)
(*          >=<0 == to encode x >=< 0                                         *)
(*          >?<0 == unknown reality                                           *)
(*                                                                            *)
(* * sign proofs                                                              *)
(*    [sgn of x] == proof that x is of sign inferred by x%:sgn                *)
(*    [gt0 of x] == proof that x > 0                                          *)
(*    [lt0 of x] == proof that x < 0                                          *)
(*    [ge0 of x] == proof that x >= 0                                         *)
(*    [le0 of x] == proof that x <= 0                                         *)
(*   [cmp0 of x] == proof that 0 >=< x                                        *)
(*   [neq0 of x] == proof that x != 0                                         *)
(*                                                                            *)
(* * constructors                                                             *)
(*   PosNum xgt0 == builds a {posnum R} from a proof xgt0 : x > 0 where x : R *)
(*   NngNum xge0 == builds a {posnum R} from a proof xgt0 : x >= 0 where x : R*)
(*   Signed.mk p == builds a {compare x0 & nz & cond} from a proof p that     *)
(*                  some x satisfies sign conditions encoded by nz and cond   *)
(*                                                                            *)
(* * misc                                                                     *)
(*          !! x == triggers pretyping to fill the holes of the term x. The   *)
(*                  main use case is to trigger typeclass inference in the    *)
(*                  body of a ssreflect have := !! body.                      *)
(*                  Credits: Enrico Tassi.                                    *)
(*             2 == notation for 2%:R.                                        *)
(*                                                                            *)
(* --> A number of canonical instances are provided for common operations, if *)
(* your favorite operator is missing, look below for examples on how to add   *)
(* the appropriate Canonical.                                                 *)
(* --> Canonical instances are also provided according to types, as a         *)
(* fallback when no known operator appears in the expression. Look to         *)
(* nat_snum below for an example on how to add your favorite type.            *)
(******************************************************************************)

Reserved Notation "{ 'compare' x0 & nz & cond }"
  (at level 0, x0 at level 200, nz at level 200,
   format "{ 'compare'  x0  &  nz  &  cond }").
Reserved Notation "{ 'num' R & nz & cond }"
  (at level 0, R at level 200, nz at level 200,
   format "{ 'num'  R  &  nz  &  cond }").
Reserved Notation "{ = x0 }" (at level 0, format "{ =  x0 }").
Reserved Notation "{ > x0 }" (at level 0, format "{ >  x0 }").
Reserved Notation "{ < x0 }" (at level 0, format "{ <  x0 }").
Reserved Notation "{ >= x0 }" (at level 0, format "{ >=  x0 }").
Reserved Notation "{ <= x0 }" (at level 0, format "{ <=  x0 }").
Reserved Notation "{ >=< x0 }" (at level 0, format "{ >=<  x0 }").
Reserved Notation "{ >< x0 }" (at level 0, format "{ ><  x0 }").
Reserved Notation "{ != x0 }" (at level 0, format "{ !=  x0 }").
Reserved Notation "{ ?= x0 }" (at level 0, format "{ ?=  x0 }").
Reserved Notation "{ = x0 : T }" (at level 0, format "{ =  x0  :  T }").
Reserved Notation "{ > x0 : T }" (at level 0, format "{ >  x0  :  T }").
Reserved Notation "{ < x0 : T }" (at level 0, format "{ <  x0  :  T }").
Reserved Notation "{ >= x0 : T }" (at level 0, format "{ >=  x0  :  T }").
Reserved Notation "{ <= x0 : T }" (at level 0, format "{ <=  x0  :  T }").
Reserved Notation "{ >=< x0 : T }" (at level 0, format "{ >=<  x0  :  T }").
Reserved Notation "{ >< x0 : T }" (at level 0, format "{ ><  x0  :  T }").
Reserved Notation "{ != x0 : T }" (at level 0, format "{ !=  x0  :  T }").
Reserved Notation "{ ?= x0 : T }" (at level 0, format "{ ?=  x0  :  T }").
Reserved Notation "=0" (at level 0, format "=0").
Reserved Notation ">=0" (at level 0, format ">=0").
Reserved Notation "<=0" (at level 0, format "<=0").
Reserved Notation ">=<0" (at level 0, format ">=<0").
Reserved Notation ">?<0" (at level 0, format ">?<0").
Reserved Notation "!=0" (at level 0, format "!=0").
Reserved Notation "?=0" (at level 0, format "?=0").

Reserved Notation "x %:sgn" (at level 2, format "x %:sgn").
Reserved Notation "x %:num" (at level 2, format "x %:num").
Reserved Notation "x %:posnum" (at level 2, format "x %:posnum").
Reserved Notation "x %:nngnum" (at level 2, format "x %:nngnum").
Reserved Notation "[ 'sgn' 'of' x ]" (format "[ 'sgn' 'of'  x ]").
Reserved Notation "[ 'gt0' 'of' x ]" (format "[ 'gt0' 'of'  x ]").
Reserved Notation "[ 'lt0' 'of' x ]" (format "[ 'lt0' 'of'  x ]").
Reserved Notation "[ 'ge0' 'of' x ]" (format "[ 'ge0' 'of'  x ]").
Reserved Notation "[ 'le0' 'of' x ]" (format "[ 'le0' 'of'  x ]").
Reserved Notation "[ 'cmp0' 'of' x ]" (format "[ 'cmp0' 'of'  x ]").
Reserved Notation "[ 'neq0' 'of' x ]" (format "[ 'neq0' 'of'  x ]").

Reserved Notation "{ 'posnum' R }" (at level 0, format "{ 'posnum'  R }").
Reserved Notation "{ 'nonneg' R }" (at level 0, format "{ 'nonneg'  R }").
Reserved Notation "x %:pos" (at level 2, format "x %:pos").
Reserved Notation "x %:nng" (at level 2, format "x %:nng").

Reserved Notation "!! x" (at level 100, only parsing).
The only parsing modifier has no effect in Reserved
Notation.
[irrelevant-reserved-notation-only-parsing,parsing]

Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
Import Order.TTheory Order.Syntax.
Import GRing.Theory Num.Theory.

Local Open Scope ring_scope.
Local Open Scope order_scope.

Declare Scope snum_scope.
Delimit Scope snum_scope with snum.
Declare Scope snum_sign_scope.
Delimit Scope snum_sign_scope with snum_sign.
Declare Scope snum_nullity_scope.
Delimit Scope snum_nullity_scope with snum_nullity.

Notation "!! x" := (ltac:(refine x)) (only parsing).
(* infer class to help typeclass inference on the fly *)
Class infer (P : Prop) := Infer : P.
#[global] Hint Mode infer ! : typeclass_instances.
#[global] Hint Extern 0 (infer _) => (exact) : typeclass_instances.
Lemma inferP (P : Prop) : P -> infer P.
P: Prop
P -> infer P Proof.
4 by []. Qed.

Module Import KnownSign.
Variant nullity := NonZero | MaybeZero.
Coercion nullity_bool nz := if nz is NonZero then true else false.
Definition nz_of_bool b := if b then NonZero else MaybeZero.

Variant sign := EqZero | NonNeg | NonPos.
Variant real := Sign of sign | AnySign.
Variant reality := Real of real | Arbitrary.

Definition wider_nullity xnz ynz :=
  match xnz, ynz with
  | MaybeZero, _
  | NonZero, NonZero => true
  | NonZero, MaybeZero => false
  end.
Definition wider_sign xs ys :=
  match xs, ys with
  | NonNeg, NonNeg | NonNeg, EqZero
  | NonPos, NonPos | NonPos, EqZero
  | EqZero, EqZero => true
  | NonNeg, NonPos | NonPos, NonNeg
  | EqZero, NonPos | EqZero, NonNeg => false
  end.
Definition wider_real xr yr :=
  match xr, yr with
  | AnySign, _ => true
  | Sign sx, Sign sy => wider_sign sx sy
  | Sign _, AnySign => false
  end.
Definition wider_reality xr yr :=
  match xr, yr with
  | Arbitrary, _ => true
  | Real xr, Real yr => wider_real xr yr
  | Real _, Arbitrary => false
  end.
End KnownSign.

Module Signed.
Section Signed.
Context (disp : unit) (T : porderType disp) (x0 : T).

Local Coercion is_real r := if r is Real _ then true else false.
Definition reality_cond (n : reality) (x : T) :=
  match n with
  | Real (Sign EqZero) => x == x0
  | Real (Sign NonNeg) => x >= x0
  | Real (Sign NonPos) => x <= x0
  | Real AnySign       => (x0 <= x) || (x <= x0)
  | Arbitary           => true
  end.

Record def (nz : nullity) (cond : reality) := Def {
  r :> T;
  #[canonical=no]
  P : (nz ==> (r != x0)) && reality_cond cond r
}.

End Signed.

Notation spec x0 nz cond x :=
  ((nullity_bool nz%snum_nullity ==> (x != x0))
   && (reality_cond x0 cond%snum_sign x)).

Record typ d nz cond := Typ {
  sort : porderType d;
  #[canonical=no]
  sort_x0 : sort;
  #[canonical=no]
  allP : forall x : sort, spec sort_x0 nz cond x
}.

Definition mk {d T} x0 nz cond r P : @def d T x0 nz cond :=
  @Def d T x0 nz cond r P.

Definition from {d T x0 nz cond}
  {x : @def d T x0 nz cond} (phx : phantom T x) := x.

Definition fromP {d T x0 nz cond}
  {x : @def d T x0 nz cond} (phx : phantom T x) := P x.

Module Exports.
Coercion Sign : sign >-> real.
Coercion Real : real >-> reality.
Coercion is_real : reality >-> bool.
Bind Scope snum_sign_scope with sign.
Bind Scope snum_sign_scope with reality.
Bind Scope snum_nullity_scope with nullity.
Notation "=0" := EqZero : snum_sign_scope.
Notation ">=0" := NonNeg : snum_sign_scope.
Notation "<=0" := NonPos : snum_sign_scope.
Notation ">=<0" := AnySign : snum_sign_scope.
Notation ">?<0" := Arbitrary : snum_sign_scope.
Notation "!=0" := NonZero : snum_nullity_scope.
Notation "?=0" := MaybeZero : snum_nullity_scope.
Notation "{ 'compare' x0 & nz & cond }" := (def x0 nz cond) : type_scope.
Notation "{ 'num' R & nz & cond }" := (def (0%R : R) nz cond) : ring_scope.
Notation "{ = x0 : T }" := (def (x0 : T) MaybeZero EqZero) : type_scope.
Notation "{ > x0 : T }" := (def (x0 : T) NonZero NonNeg) : type_scope.
Notation "{ < x0 : T }" := (def (x0 : T) NonZero NonPos) : type_scope.
Notation "{ >= x0 : T }" := (def (x0 : T) MaybeZero NonNeg) : type_scope.
Notation "{ <= x0 : T }" := (def (x0 : T) MaybeZero NonPos) : type_scope.
Notation "{ >< x0 : T }" := (def (x0 : T) NonZero Real) : type_scope.
Notation "{ >=< x0 : T }" := (def (x0 : T) MaybeZero Real) : type_scope.
Notation "{ != x0 : T }" := (def (x0 : T) NonZero Arbitrary) : type_scope.
Notation "{ ?= x0 : T }" := (def (x0 : T) MaybeZero Arbitrary) : type_scope.
Notation "{ = x0 }" := (def x0 MaybeZero EqZero) : type_scope.
Notation "{ > x0 }" := (def x0 NonZero NonNeg) : type_scope.
Notation "{ < x0 }" := (def x0 NonZero NonPos) : type_scope.
Notation "{ >= x0 }" := (def x0 MaybeZero NonNeg) : type_scope.
Notation "{ <= x0 }" := (def x0 MaybeZero NonPos) : type_scope.
Notation "{ >< x0 }" := (def x0 NonZero Real) : type_scope.
Notation "{ >=< x0 }" := (def x0 MaybeZero Real) : type_scope.
Notation "{ != x0 }" := (def x0 NonZero Arbitrary) : type_scope.
Notation "{ ?= x0 }" := (def x0 MaybeZero Arbitrary) : type_scope.
Notation "x %:sgn" := (from (Phantom _ x)) : ring_scope.
Notation "[ 'sgn' 'of' x ]" := (fromP (Phantom _ x)) : ring_scope.
Notation num := r.
Notation "x %:num" := (r x) : ring_scope.
Definition posnum (R : numDomainType) of phant R := {> 0%R : R}.
Notation "{ 'posnum' R }" := (@posnum _ (Phant R))  : ring_scope.
Notation "x %:posnum" := (@num _ _ 0%R !=0 >=0 x) : ring_scope.
Definition nonneg (R : numDomainType) of phant R := {>= 0%R : R}.
Notation "{ 'nonneg' R }" := (@nonneg _ (Phant R))  : ring_scope.
Notation "x %:nngnum" := (@num _ _ 0%R ?=0 >=0 x) : ring_scope.
Notation "2" := 2%:R : ring_scope.
Arguments r {disp T x0 nz cond}.
End Exports.
End Signed.
Export Signed.Exports.

Section POrder.
Variables (d : unit) (T : porderType d) (x0 : T) (nz : nullity) (cond : reality).
Local Notation sT := {compare x0 & nz & cond}.
Canonical signed_subType := [subType for @Signed.r d T x0 nz cond].
Definition signed_eqMixin := [eqMixin of sT by <:].
Canonical signed_eqType := EqType sT signed_eqMixin.
Definition signed_choiceMixin := [choiceMixin of sT by <:].
Canonical signed_choiceType := ChoiceType sT signed_choiceMixin.
Definition signed_porderMixin := [porderMixin of sT by <:].
Canonical signed_porderType := POrderType d sT signed_porderMixin.
End POrder.

Lemma top_typ_subproof d (T : porderType d) (x0 x : T) :
  Signed.spec x0 ?=0 >?<0 x.
d: unit
T: porderType d
x0, x: T
(?=0%snum_nullity ==> (x != x0)) &&
Signed.reality_cond x0 >?<0 x
Proof.
b by []. Qed.

Canonical top_typ d (T : porderType d) (x0 : T) :=
  Signed.Typ (top_typ_subproof x0).

Lemma real_domain_typ_subproof (R : realDomainType) (x : R) :
  Signed.spec 0%R ?=0 >=<0 x.
R: realDomainType
x: R
(?=0%snum_nullity ==> (x != 0%R)) &&
Signed.reality_cond 0%R >=<0 x
Proof.
14 by rewrite /= -realE num_real. Qed.

Canonical real_domain_typ (R : realDomainType) :=
  Signed.Typ (@real_domain_typ_subproof R).

Lemma real_field_typ_subproof (R : realFieldType) (x : R) :
  Signed.spec 0%R ?=0 >=<0 x.
R: realFieldType
18
19
Proof.
1c exact: real_domain_typ_subproof. Qed.

Canonical real_field_typ (R : realFieldType) :=
  Signed.Typ (@real_field_typ_subproof R).

Lemma nat_typ_subproof (x : nat) : Signed.spec 0%N ?=0 >=0 x.
x: nat
(?=0%snum_nullity ==> (x != 0%N)) &&
Signed.reality_cond 0%N >=0 x
Proof.
22 by []. Qed.

Canonical nat_typ := Signed.Typ nat_typ_subproof.

Lemma typ_snum_subproof d nz cond (xt : Signed.typ d nz cond)
    (x : Signed.sort xt) :
  Signed.spec (Signed.sort_x0 xt) nz cond x.
e
nz: nullity
cond: reality
xt: Signed.typ d nz cond
x: Signed.sort xt
(nz ==> (x != Signed.sort_x0 xt)) &&
Signed.reality_cond (Signed.sort_x0 xt) cond x
Proof.
29 by move: xt x => []. Qed.

(* This adds _ <- Signed.r ( typ_snum )
   to canonical projections (c.f., Print Canonical Projections
   Signed.r) meaning that if no other canonical instance (with a
   registered head symbol) is found, a canonical instance of
   Signed.typ, like the ones above, will be looked for. *)
Canonical typ_snum d nz cond (xt : Signed.typ d nz cond) (x : Signed.sort xt) :=
  Signed.mk (typ_snum_subproof x).

(* Section Order. *)
(* Variables (d : unit) (T : orderType d) (x0 : T) (nz : nullity) (cond : reality). *)
(* Local Notation sT := {compare x0 & nz & cond}. *)

(* Lemma signed_le_total : totalPOrderMixin [porderType of sT]. *)
(* Proof. by move=> x y; apply: le_total. Qed. *)

(* Canonical signed_latticeType := LatticeType sT signed_le_total. *)
(* Canonical signed_distrLatticeType := DistrLatticeType sT signed_le_total. *)
(* Canonical signed_orderType := OrderType sT signed_le_total. *)

(* End Order. *)

Class unify {T} f (x y : T) := Unify : f x y = true.
#[global] Hint Mode unify - - - + : typeclass_instances.
Class unify' {T} f (x y : T) := Unify' : f x y = true.
#[global] Instance unify'P {T} f (x y : T) : unify' f x y -> unify f x y := id.
#[global]
Hint Extern 0 (unify' _ _ _) => vm_compute; reflexivity : typeclass_instances.

Notation unify_nz nzx nzy :=
  (unify wider_nullity nzx%snum_nullity nzy%snum_nullity).
Notation unify_r rx ry :=
  (unify wider_reality rx%snum_sign ry%snum_sign).

#[global] Instance anysign_wider_real sign : unify_r (Real AnySign) (Real sign).
sign: real
unify_r >=<0 sign
Proof.
33 by []. Qed.

#[global] Instance any_reality_wider_eq0 cond : unify_r cond =0.
2d
unify_r cond =0
Proof.
3a by case: cond => [[[]|]|]. Qed.

Section Theory.
Context {d : unit} {T : porderType d} {x0 : T}
  {nz : nullity} {cond : reality}.
Local Notation sT := {compare x0 & nz & cond}.
Implicit Type x : sT.

Lemma signed_intro {x} : x%:num = x%:num :> T.
e
f
x0: T
2c
2d
x: sT
x%:num = x%:num Proof.
40 by []. Qed.

Lemma bottom x : unify_nz !=0 nz -> unify_r =0 cond -> False.
42
unify_nz !=0 nz -> unify_r =0 cond -> False
Proof.
48
by move: x => [x /= /andP[]]; move: cond nz => [[[]|]|] [] //= /[swap] ->.
Qed.

Lemma gt0 x : unify_nz !=0 nz -> unify_r >=0 cond -> x0 < x%:num :> T.
42
unify_nz !=0 nz ->
unify_r >=0 cond -> (x0 : T) < (x%:num : T)
Proof.
4d
move: x => [x /= /andP[]].
e
f
43
2c
2d
x: T
nz ==> (x != x0) ->
Signed.reality_cond x0 cond x ->
unify_nz !=0 nz -> unify_r >=0 cond -> x0 < x
by move: cond nz => [[[]|]|] [] //=; rewrite lt_def => -> // /eqP -> /=.
Qed.

Lemma le0F x : unify_nz !=0 nz -> unify_r >=0 cond -> x%:num <= x0 :> T = false.
42
unify_nz !=0 nz ->
unify_r >=0 cond -> ((x%:num : T) <= (x0 : T)) = false
Proof.
58 by move=> ? ?; rewrite lt_geF//; apply: gt0. Qed.

Lemma lt0 x : unify_nz !=0 nz -> unify_r <=0 cond -> x%:num < x0 :> T.
42
unify_nz !=0 nz ->
unify_r <=0 cond -> (x%:num : T) < (x0 : T)
Proof.
5d
move: x => [x /= /andP[]].
54
nz ==> (x != x0) ->
Signed.reality_cond x0 cond x ->
unify_nz !=0 nz -> unify_r <=0 cond -> x < x0
move: cond nz => [[[]|]|] [] //=; rewrite lt_def [x0 == _]eq_sym => -> //.
54
x == x0 ->
unify_nz !=0 !=0 ->
unify_r <=0 =0 -> true && (x <= x0)
by move=> /eqP -> /=.
Qed.

Lemma ge0F x : unify_nz !=0 nz -> unify_r <=0 cond -> x0 <= x%:num :> T = false.
42
unify_nz !=0 nz ->
unify_r <=0 cond -> ((x0 : T) <= (x%:num : T)) = false
Proof.
6a by move=> ? ?; rewrite lt_geF//; apply: lt0. Qed.

Lemma ge0 x : unify_r >=0 cond -> x0 <= x%:num :> T.
42
unify_r >=0 cond -> (x0 : T) <= (x%:num : T)
Proof.
6f
by case: x => [x /= /andP[]]; move: cond nz => [[[]|]|] [] //= _ /eqP ->.
Qed.

Lemma lt0F x : unify_r >=0 cond -> x%:num < x0 :> T = false.
42
unify_r >=0 cond -> ((x%:num : T) < (x0 : T)) = false
Proof.
74 by move=> ?; rewrite le_gtF//; apply: ge0. Qed.

Lemma le0 x : unify_r <=0 cond -> x0 >= x%:num :> T.
42
unify_r <=0 cond -> (x%:num : T) <= (x0 : T)
Proof.
79
by case: x => [x /= /andP[]]; move: cond nz => [[[]|]|] [] //= _ /eqP ->.
Qed.

Lemma gt0F x : unify_r <=0 cond -> x0 < x%:num :> T = false.
42
unify_r <=0 cond -> ((x0 : T) < (x%:num : T)) = false
Proof.
7e by move=> ?; rewrite le_gtF//; apply: le0. Qed.

Lemma cmp0 x : unify_r (Real AnySign) cond -> (x0 >=< x%:num).
42
unify_r >=<0 cond -> x0 >=< x%:num
Proof.
83
case: x => [x /= /andP[]].
54
nz ==> (x != x0) ->
Signed.reality_cond x0 cond x ->
unify_r >=<0 cond -> x0 >=< x
by move: cond nz => [[[]|]|] [] //= _;
  do ?[by move=> /eqP ->; rewrite comparablexx];
  move=> sx; rewrite /Order.comparable sx// orbT.
Qed.

Lemma neq0 x : unify_nz !=0 nz -> x%:num != x0 :> T.
42
unify_nz !=0 nz -> x%:num != x0 :> T
Proof.
8c by case: x => [x /= /andP[]]; move: cond nz => [[[]|]|] []. Qed.

Lemma eq0F x : unify_nz !=0 nz -> x%:num == x0 :> T = false.
42
unify_nz !=0 nz -> (x%:num == x0 :> T) = false
Proof.
91 by move=> /neq0-/(_ x)/negPf->. Qed.

Lemma eq0 x : unify_r =0 cond -> x%:num = x0.
42
unify_r =0 cond -> x%:num = x0
Proof.
96
by case: x => [x /= /andP[_]]; move: cond nz => [[[]|]|] [] //= /eqP ->.
Qed.

Lemma widen_signed_subproof x nz' cond' :
  unify_nz nz' nz -> unify_r cond' cond ->
  Signed.spec x0 nz' cond' x%:num.
e
f
43
2c
2d
44
nz': nullity
cond': reality
unify_nz nz' nz ->
unify_r cond' cond ->
(nz' ==> (x%:num != x0)) &&
Signed.reality_cond x0 cond' x%:num
Proof.
9b
case: x => [x /= /andP[]].
e
f
43
2c
2d
9e
9f
55
nz ==> (x != x0) ->
Signed.reality_cond x0 cond x ->
unify_nz nz' nz ->
unify_r cond' cond ->
(nz' ==> (x != x0)) && Signed.reality_cond x0 cond' x
by case: cond nz cond' nz' => [[[]|]|] [] [[[]|]|] [] //= nz'' cond'';
   rewrite ?nz'' ?cond'' ?orbT //; move: cond'' nz'' => /eqP ->; rewrite lexx.
Qed.

Definition widen_signed x nz' cond'
    (unz : unify_nz nz' nz) (ucond : unify_r cond' cond) :=
  Signed.mk (widen_signed_subproof x unz ucond).

Lemma widen_signedE x (unz : unify_nz nz nz) (ucond : unify_r cond cond) :
  @widen_signed x nz cond unz ucond = x.
e
f
43
2c
2d
44
unz: unify_nz nz nz
ucond: unify_r cond cond
widen_signed x unz ucond = x
Proof.
a8 exact/val_inj. Qed.

Lemma posE (x : sT) (unz : unify_nz !=0 nz) (ucond : unify_r >=0 cond) :
  (widen_signed x%:num%:sgn unz ucond)%:num = x%:num.
e
f
43
2c
2d
44
unz: unify_nz !=0 nz
ucond: unify_r >=0 cond
(widen_signed (x%:num)%:sgn unz ucond)%:num = x%:num
Proof.
b0 by []. Qed.

Lemma nngE (x : sT) (unz : unify_nz ?=0 nz) (ucond : unify_r >=0 cond) :
  (widen_signed x%:num%:sgn unz ucond)%:num = x%:num.
e
f
43
2c
2d
44
unz: unify_nz ?=0 nz
b4
b5
Proof.
b8 by []. Qed.

End Theory.

Arguments bottom {d T x0 nz cond} _ {_ _}.
Arguments gt0 {d T x0 nz cond} _ {_ _}.
Arguments le0F {d T x0 nz cond} _ {_ _}.
Arguments lt0 {d T x0 nz cond} _ {_ _}.
Arguments ge0F {d T x0 nz cond} _ {_ _}.
Arguments ge0 {d T x0 nz cond} _ {_}.
Arguments lt0F {d T x0 nz cond} _ {_}.
Arguments le0 {d T x0 nz cond} _ {_}.
Arguments gt0F {d T x0 nz cond} _ {_}.
Arguments cmp0 {d T x0 nz cond} _ {_}.
Arguments neq0 {d T x0 nz cond} _ {_}.
Arguments eq0F {d T x0 nz cond} _ {_}.
Arguments eq0 {d T x0 nz cond} _ {_}.
Arguments widen_signed {d T x0 nz cond} _ {_ _ _ _}.
Arguments widen_signedE {d T x0 nz cond} _ {_ _}.
Arguments posE {d T x0 nz cond} _ {_ _}.
Arguments nngE {d T x0 nz cond} _ {_ _}.

Notation "[ 'gt0' 'of' x ]" := (ltac:(refine (gt0 x%:sgn))).
This notation contains Ltac expressions: it will not
be used for printing.
[non-reversible-notation,parsing]
Notation "[ 'lt0' 'of' x ]" := (ltac:(refine (lt0 x%:sgn))).
This notation contains Ltac expressions: it will not
be used for printing.
[non-reversible-notation,parsing]
Notation "[ 'ge0' 'of' x ]" := (ltac:(refine (ge0 x%:sgn))).
This notation contains Ltac expressions: it will not
be used for printing.
[non-reversible-notation,parsing]
Notation "[ 'le0' 'of' x ]" := (ltac:(refine (le0 x%:sgn))).
This notation contains Ltac expressions: it will not
be used for printing.
[non-reversible-notation,parsing]
Notation "[ 'cmp0' 'of' x ]" := (ltac:(refine (cmp0 x%:sgn))).
This notation contains Ltac expressions: it will not
be used for printing.
[non-reversible-notation,parsing]
Notation "[ 'neq0' 'of' x ]" := (ltac:(refine (neq0 x%:sgn))).
This notation contains Ltac expressions: it will not
be used for printing.
[non-reversible-notation,parsing]

#[global] Hint Extern 0 (is_true (0%R < _)%O) => solve [apply: gt0] : core.
#[global] Hint Extern 0 (is_true (_ < 0%R)%O) => solve [apply: lt0] : core.
#[global] Hint Extern 0 (is_true (0%R <= _)%O) => solve [apply: ge0] : core.
#[global] Hint Extern 0 (is_true (_ <= 0%R)%O) => solve [apply: le0] : core.
#[global] Hint Extern 0 (is_true (_ \is Num.real)) => solve [apply: cmp0] : core.
#[global] Hint Extern 0 (is_true (0%R >=< _)%O) => solve [apply: cmp0] : core.
#[global] Hint Extern 0 (is_true (_ != 0%R)%O) => solve [apply: neq0] : core.

Notation "x %:pos" := (widen_signed x%:sgn : {posnum _}) (only parsing)
  : ring_scope.
Notation "x %:nng" := (widen_signed x%:sgn : {nonneg _}) (only parsing)
  : ring_scope.
Notation "x %:pos" := (@widen_signed _ _ _ _ _
    (@Signed.from _ _ _ _ _ _ (Phantom _ x)) !=0 (Real (Sign >=0)) _ _)
  (only printing) : ring_scope.
Notation "x %:nng" := (@widen_signed _ _ _ _ _
    (@Signed.from _ _ _ _ _ _ (Phantom _ x)) ?=0 (Real (Sign >=0)) _ _)
  (only printing) : ring_scope.

Local Open Scope ring_scope.

Section Order.
Variables (R : numDomainType) (nz : nullity) (r : real).
Local Notation nR := {num R & nz & r}.

Lemma signed_le_total : totalPOrderMixin [porderType of nR].
R: numDomainType
2c
r: real
totalPOrderMixin [porderType of {num R & nz & r}]
Proof.
c4 by move=> x y; apply: real_comparable => /=. Qed.

Canonical signed_latticeType := LatticeType nR signed_le_total.
Canonical signed_distrLatticeType := DistrLatticeType nR signed_le_total.
Canonical signed_orderType := OrderType nR signed_le_total.

End Order.

Section POrderStability.
Context {disp : unit} {T : porderType disp} {x0 : T}.

Definition min_nonzero_subdef (xnz ynz : nullity) (xr yr : reality) :=
  nz_of_bool
    (xnz && ynz
     || xnz && yr && match xr with Real (Sign <=0) => true | _ => false end
     || ynz && match yr with Real (Sign <=0) => true | _ => false end).
Arguments min_nonzero_subdef /.

Definition min_reality_subdef (xnz ynz : nullity) (xr yr : reality) : reality :=
  match xr, yr with
  | Real (Sign =0), Real (Sign =0)
  | Real (Sign =0), Real (Sign >=0)
  | Real (Sign >=0), Real (Sign =0) => =0
  | Real (Sign >=0), Real (Sign >=0) => >=0
  | Real (Sign <=0), Real _
  | Real _, Real (Sign <=0) => <=0
  | Real _, Real _ => >=<0
  | _, _ => >?<0
  end.
Arguments min_reality_subdef /.

Lemma min_snum_subproof (xnz ynz : nullity) (xr yr : reality)
    (x : {compare x0 & xnz & xr}) (y : {compare x0 & ynz & yr})
    (rnz := min_nonzero_subdef xnz ynz xr yr)
    (rrl := min_reality_subdef xnz ynz xr yr) :
  Signed.spec x0 rnz rrl (Order.min x%:num y%:num).
disp: unit
T: porderType disp
43
xnz, ynz: nullity
xr, yr: reality
x: {compare x0 & xnz & xr}
y: {compare x0 & ynz & yr}
rnz:= min_nonzero_subdef xnz ynz xr yr: nullity
rrl:= min_reality_subdef xnz ynz xr yr: reality
(rnz ==> (Order.min x%:num y%:num != x0)) &&
Signed.reality_cond x0 rrl (Order.min x%:num y%:num)
Proof.
cc
rewrite {}/rnz {}/rrl; apply/andP; split.
cf
d0
43
d1
d2
d3
d4
min_nonzero_subdef xnz ynz xr yr ==>
(Order.min x%:num y%:num != x0)
dc
Signed.reality_cond x0
  (min_reality_subdef xnz ynz xr yr)
  (Order.min x%:num y%:num)
  move: xr yr xnz ynz x y => [[[]|]|] [[[]|]|] [] []//= x y; rewrite /Order.min;
    do ?[by case: (bottom x)|by case: (bottom y)
        |by case: ifP; rewrite ?eq0F// => xlty;
            have := !! lt_trans xlty (lt0 y); rewrite lt_neqAle => /andP[]
        |by rewrite ifT ?eq0F//; apply: lt_le_trans (ge0 y); exact: lt0
        |by have := !! le0 y;
            rewrite le_eqVlt => /predU1P[->|]; rewrite ?lt0 ?eq0F//;
            case: ifP => _; rewrite ?eq0F// lt_neqAle => /andP[]].
cf
d0
43
x: {compare x0 & !=0 & <=0}
y: {compare x0 & ?=0 & >=<0}
(if (x%:num < y%:num)%O then x%:num else y%:num) != x0
de
  have /orP[x0ley|] := !! cmp0 y.
cf
d0
43
e5
e6
x0ley: (x0 <= y%:num)%O
e7
e4
(y%:num <= x0)%O ->
(if (x%:num < y%:num)%O then x%:num else y%:num) != x0
df
    by rewrite ifT ?eq0F//; apply: lt_le_trans x0ley; exact: lt0.
e4
ef
de
    rewrite le_eqVlt => /predU1P[->|]; rewrite ?lt0 ?eq0F//.
e4
(y%:num < x0)%O ->
(if (x%:num < y%:num)%O then x%:num else y%:num) != x0
de
  by case: ifP => _; rewrite ?eq0F// lt_neqAle => /andP[].
dc
e0
move: xr yr xnz ynz x y => [[[]|]|] [[[]|]|] [] []//= x y;
  do ?[by case: (bottom x)|by case: (bottom y)
      |by apply: comparable_minr; exact: cmp0
      |by rewrite minEle; case: ifP; rewrite ge0
      |by rewrite ?eq0 minEle ?ge0
      |by rewrite ?eq0 minElt; case: ifP; rewrite ?eq0// lt0F
      |by rewrite minEle; case: ifP => [xlty|]; rewrite ?le0//;
          apply: (le_trans xlty); rewrite le0
      |by have /orP[x0ley|] := !! cmp0 y;
          [rewrite minEle ifT ?le0//; apply: le_trans x0ley; exact: le0
          |rewrite minEle; case: ifP => //; exact: le_trans]].
Qed.

Canonical min_snum (xnz ynz : nullity) (xr yr : reality)
    (x : {compare x0 & xnz & xr}) (y : {compare x0 & ynz & yr}) :=
  Signed.mk (min_snum_subproof x y).

Definition max_nonzero_subdef (xnz ynz : nullity) (xr yr : reality) :=
  nz_of_bool
    (xnz && ynz
     || xnz && match xr with Real (Sign >=0) => true | _ => false end
     || ynz && xr && match yr with Real (Sign >=0) => true | _ => false end).
Arguments max_nonzero_subdef /.

Definition max_reality_subdef (xnz ynz : nullity) (xr yr : reality) : reality :=
  match xr, yr with
  | Real (Sign =0), Real (Sign =0)
  | Real (Sign =0), Real (Sign <=0)
  | Real (Sign <=0), Real (Sign =0) => =0
  | Real (Sign <=0), Real (Sign <=0) => <=0
  | Real (Sign >=0), Real _
  | Real _, Real (Sign >=0) => >=0
  | Real _, Real _ => >=<0
  | _, _ => >?<0
  end.
Arguments max_reality_subdef /.

Lemma max_snum_subproof (xnz ynz : nullity) (xr yr : reality)
    (x : {compare x0 & xnz & xr}) (y : {compare x0 & ynz & yr})
    (rnz := max_nonzero_subdef xnz ynz xr yr)
    (rrl := max_reality_subdef xnz ynz xr yr) :
  Signed.spec x0 rnz rrl (Order.max x%:num y%:num).
cf
d0
43
d1
d2
d3
d4
rnz:= max_nonzero_subdef xnz ynz xr yr: nullity
rrl:= max_reality_subdef xnz ynz xr yr: reality
(rnz ==> (Order.max x%:num y%:num != x0)) &&
Signed.reality_cond x0 rrl (Order.max x%:num y%:num)
Proof.
fb
rewrite {}/rnz {}/rrl; apply/andP; split.
dc
max_nonzero_subdef xnz ynz xr yr ==>
(Order.max x%:num y%:num != x0)
dc
Signed.reality_cond x0
  (max_reality_subdef xnz ynz xr yr)
  (Order.max x%:num y%:num)
  move: xr yr xnz ynz x y => [[[]|]|] [[[]|]|] [] []//= x y; rewrite maxElt;
    do ?[by case: (bottom x)|by case: (bottom y)
        |by case: ifP => [xlty|]; rewrite ?eq0F//;
            do [suff : (x0 < y%:num)%O by rewrite lt_def => /andP[]];
            apply: le_lt_trans xlty; exact: ge0
        |by rewrite ifT ?eq0F//; apply: le_lt_trans (gt0 y); exact: le0
        |by have := !! ge0 x;
            rewrite le_eqVlt => /predU1P[<-|]; rewrite ?gt0 ?eq0F//;
            case: ifP => _; rewrite ?eq0F// lt_def => /andP[]].
cf
d0
43
x: {compare x0 & ?=0 & >=<0}
y: {compare x0 & !=0 & >=0}
(if (x%:num < y%:num)%O then y%:num else x%:num) != x0
106
  have /orP[|xlex0] := !! cmp0 x.
10c
(x0 <= x%:num)%O ->
(if (x%:num < y%:num)%O then y%:num else x%:num) != x0
cf
d0
43
10d
10e
xlex0: (x%:num <= x0)%O
10f
107
    rewrite le_eqVlt => /predU1P[<-|]; rewrite ?gt0 ?eq0F//.
10c
(x0 < x%:num)%O ->
(if (x%:num < y%:num)%O then y%:num else x%:num) != x0
114
    by case: ifP => _; rewrite ?eq0F// lt_def => /andP[].
116
10f
106
  by rewrite ifT ?eq0F//; apply: (le_lt_trans xlex0); exact: gt0.
dc
108
move: xr yr xnz ynz x y => [[[]|]|] [[[]|]|] [] []//= x y;
  do ?[by case: (bottom x)|by case: (bottom y)
      |by apply: comparable_maxr; exact: cmp0
      |by rewrite ?eq0 maxEle ?le0
      |by rewrite ?eq0 maxElt ifF// le_gtF// le0
      |by rewrite maxEle; case: ifP; rewrite ?ge0//; exact/le_trans/ge0
      |by rewrite maxElt; case: ifP => [xlty|]; rewrite ?le0//
      |by have /orP[|xlex0] := !! cmp0 x;
          [rewrite maxEle; case: ifP => // /[swap]; exact: le_trans
          |rewrite maxEle ifT ?ge0//; apply: (le_trans xlex0); exact: ge0]].
Qed.

Canonical max_snum (xnz ynz : nullity) (xr yr : reality)
    (x : {compare x0 & xnz & xr}) (y : {compare x0 & ynz & yr}) :=
  Signed.mk (max_snum_subproof x y).

End POrderStability.

Section NumDomainStability.
Context {R : numDomainType}.

Lemma zero_snum_subproof : Signed.spec 0 ?=0 =0 (0 : R).
c7
(?=0%snum_nullity ==> ((0 : R) != 0)) &&
Signed.reality_cond 0 =0 (0 : R)
Proof.
123 exact: eqxx. Qed.

Canonical zero_snum := Signed.mk zero_snum_subproof.

Lemma one_snum_subproof : Signed.spec 0 !=0 >=0 (1 : R).
125
(!=0%snum_nullity ==> ((1 : R) != 0)) &&
Signed.reality_cond 0 >=0 (1 : R)
Proof.
129 by rewrite /= oner_eq0 ler01. Qed.

Canonical one_snum := Signed.mk one_snum_subproof.

Definition opp_reality_subdef (xnz : nullity) (xr : reality) : reality :=
  match xr with
  | Real (Sign =0) => =0
  | Real (Sign >=0) => <=0
  | Real (Sign <=0) => >=0
  | Real AnySign    => >=<0
  | Arbitrary              => >?<0
  end.

Lemma opp_snum_subproof (xnz : nullity) (xr : reality)
    (x : {num R & xnz & xr}) (r := opp_reality_subdef xnz xr) :
  Signed.spec 0 xnz r (- x%:num).
c7
xnz: nullity
xr: reality
x: {num R & xnz & xr}
r:= opp_reality_subdef xnz xr: reality
(xnz ==> (- x%:num != 0)) &&
Signed.reality_cond 0 r (- x%:num)
Proof.
12e
by rewrite {}/r; case: xr x => [[[]|]|]//= [r]/=;
   rewrite oppr_eq0 ?(oppr_ge0, oppr_le0)// orbC.
Qed.

Canonical opp_snum (xnz : nullity) (xr : reality) (x : {num R & xnz & xr}) :=
  Signed.mk (opp_snum_subproof x).

Definition add_samesign_subdef (xnz ynz : nullity) (xr yr : reality) :=
  match xr, yr with
  | Real (Sign >=0), Real (Sign =0)
  | Real (Sign =0), Real (Sign >=0)
  | Real (Sign <=0), Real (Sign =0)
  | Real (Sign =0), Real (Sign <=0)
  | Real (Sign =0), Real (Sign =0)
  | Real (Sign >=0), Real (Sign >=0)
  | Real (Sign <=0), Real (Sign <=0) => true
  | _, _ => false
  end.

Definition add_nonzero_subdef (xnz ynz : nullity) (xr yr : reality) :=
  nz_of_bool (add_samesign_subdef xnz ynz xr yr && (xnz || ynz)).
Arguments add_nonzero_subdef /.

Definition add_reality_subdef (xnz ynz : nullity) (xr yr : reality) : reality :=
  match xr, yr with
  | Real (Sign =0), Real (Sign =0) => =0
  | Real (Sign >=0), Real (Sign =0)
  | Real (Sign =0), Real (Sign >=0)
  | Real (Sign >=0), Real (Sign >=0) => >=0
  | Real (Sign <=0), Real (Sign =0)
  | Real (Sign =0), Real (Sign <=0)
  | Real (Sign <=0), Real (Sign <=0) => <=0
  | Real _, Real _ => >=<0
  | _, _ => >?<0
  end.
Arguments add_reality_subdef /.

Lemma add_snum_subproof (xnz ynz : nullity) (xr yr : reality)
    (x : {num R & xnz & xr}) (y : {num R & ynz & yr})
    (rnz := add_nonzero_subdef xnz ynz xr yr)
    (rrl := add_reality_subdef xnz ynz xr yr) :
  Signed.spec 0 rnz rrl (x%:num + y%:num).
c7
d1
d2
133
y: {num R & ynz & yr}
rnz:= add_nonzero_subdef xnz ynz xr yr: nullity
rrl:= add_reality_subdef xnz ynz xr yr: reality
(rnz ==> (x%:num + y%:num != 0)) &&
Signed.reality_cond 0 rrl (x%:num + y%:num)
Proof.
138
rewrite {}/rnz {}/rrl; apply/andP; split.
c7
d1
d2
133
13b
add_nonzero_subdef xnz ynz xr yr ==>
(x%:num + y%:num != 0)
143
Signed.reality_cond 0
  (add_reality_subdef xnz ynz xr yr) (x%:num + y%:num)
  move: xr yr xnz ynz x y => [[[]|]|] [[[]|]|] [] []//= x y;
  by rewrite 1?addr_ss_eq0 ?(eq0F, ge0, le0, andbF, orbT).
143
147
have addr_le0 a b : a <= 0 -> b <= 0 -> a + b <= 0.
c7
d1
d2
133
13b
_t_: numDomainType
a, b: _t_
a <= 0 -> b <= 0 -> a + b <= 0
c7
d1
d2
133
13b
addr_le0: forall (t : numDomainType) (a b : t),
a <= 0 -> b <= 0 -> a + b <= 0
147
  by rewrite -!oppr_ge0 opprD; apply: addr_ge0.
154
147
move: xr yr xnz ynz x y => [[[]|]|] [[[]|]|] [] []//= x y;
  do ?[by rewrite addr_ge0|by rewrite addr_le0|by rewrite -realE realD
      |by case: (bottom x)|by case: (bottom y)|by rewrite !eq0 addr0].
Qed.

Canonical add_snum (xnz ynz : nullity) (xr yr : reality)
    (x : {num R & xnz & xr}) (y : {num R & ynz & yr}) :=
  Signed.mk (add_snum_subproof x y).

Definition mul_nonzero_subdef (xnz ynz : nullity) (xr yr : reality) :=
  nz_of_bool (xnz && ynz).
Arguments mul_nonzero_subdef /.

Definition mul_reality_subdef (xnz ynz : nullity) (xr yr : reality) : reality :=
  match xr, yr with
  | Real (Sign =0), _ | _, Real (Sign =0) => =0
  | Real (Sign >=0), Real (Sign >=0)
  | Real (Sign <=0), Real (Sign <=0) => >=0
  | Real (Sign >=0), Real (Sign <=0)
  | Real (Sign <=0), Real (Sign >=0) => <=0
  | Real _,          Real _          => >=<0
  | _ , _                            => >?<0
  end.
Arguments mul_reality_subdef /.

Lemma mul_snum_subproof (xnz ynz : nullity) (xr yr : reality)
    (x : {num R & xnz & xr}) (y : {num R & ynz & yr})
    (rnz := mul_nonzero_subdef xnz ynz xr yr)
    (rrl := mul_reality_subdef xnz ynz xr yr) :
  Signed.spec 0 rnz rrl (x%:num * y%:num).
c7
d1
d2
133
13b
rnz:= mul_nonzero_subdef xnz ynz xr yr: nullity
rrl:= mul_reality_subdef xnz ynz xr yr: reality
(rnz ==> (x%:num * y%:num != 0)) &&
Signed.reality_cond 0 rrl (x%:num * y%:num)
Proof.
15a
rewrite {}/rnz {}/rrl; apply/andP; split.
143
mul_nonzero_subdef xnz ynz xr yr ==>
(x%:num * y%:num != 0)
143
Signed.reality_cond 0
  (mul_reality_subdef xnz ynz xr yr) (x%:num * y%:num)
  by move: xr yr xnz ynz x y => [[[]|]|] [[[]|]|] [] []// x y;
     rewrite mulf_neq0.
143
167
by move: xr yr xnz ynz x y => [[[]|]|] [[[]|]|] [] []/= x y //;
   do ?[by rewrite mulr_ge0|by rewrite mulr_le0_ge0
       |by rewrite mulr_ge0_le0|by rewrite mulr_le0|by rewrite -realE realM
       |by case: (bottom x)|by case: (bottom y)|by rewrite eq0 ?mulr0// mul0r].
Qed.

Canonical mul_snum (xnz ynz : nullity) (xr yr : reality)
    (x : {num R & xnz & xr}) (y : {num R & ynz & yr}) :=
  Signed.mk (mul_snum_subproof x y).

Lemma natmul_snum_subproof (xnz nnz : nullity) (xr nr : reality)
    (x : {num R & xnz & xr}) (n : {compare 0%N & nnz & nr})
    (rnz := mul_nonzero_subdef xnz nnz xr nr)
    (rrl := mul_reality_subdef xnz nnz xr nr) :
  Signed.spec 0 rnz rrl (x%:num *+ n%:num).
c7
xnz, nnz: nullity
xr, nr: reality
133
n: {compare 0%N & nnz & nr}
rnz:= mul_nonzero_subdef xnz nnz xr nr: nullity
rrl:= mul_reality_subdef xnz nnz xr nr: reality
(rnz ==> (x%:num *+ n%:num != 0)) &&
Signed.reality_cond 0 rrl (x%:num *+ n%:num)
Proof.
16c
rewrite {}/rnz {}/rrl; apply/andP; split.
c7
16f
170
133
171
mul_nonzero_subdef xnz nnz xr nr ==>
(x%:num *+ n%:num != 0)
179
Signed.reality_cond 0
  (mul_reality_subdef xnz nnz xr nr)
  (x%:num *+ n%:num)
  by move: xr nr xnz nnz x n => [[[]|]|] [[[]|]|] [] []// x n;
     rewrite mulrn_eq0//= ?eq0F.
179
17d
move: xr nr xnz nnz x n => [[[]|]|] [[[]|]|] [] []/= x [[|n]//= _] //;
  do ?[by case: (bottom x)|by case: (bottom n)
      |by rewrite mulrn_wge0|by rewrite mulrn_wle0|by rewrite eq0 mul0rn
      |by apply: real_comparable; rewrite ?real0 ?realrMn].
Qed.

Canonical natmul_snum (xnz nnz : nullity) (xr nr : reality)
    (x : {num R & xnz & xr}) (n : {compare 0%N & nnz & nr}) :=
  Signed.mk (natmul_snum_subproof x n).

Lemma intmul_snum_subproof (xnz nnz : nullity) (xr nr : reality)
    (x : {num R & xnz & xr}) (n : {num int & nnz & nr})
    (rnz := mul_nonzero_subdef xnz nnz xr nr)
    (rrl := mul_reality_subdef xnz nnz xr nr) :
  Signed.spec 0 rnz rrl (x%:num *~ n%:num).
c7
16f
170
133
n: {num int & nnz & nr}
172
173
(rnz ==> (x%:num *~ n%:num != 0)) &&
Signed.reality_cond 0 rrl (x%:num *~ n%:num)
Proof.
182
rewrite {}/rnz {}/rrl; apply/andP; split.
c7
16f
170
133
185
mul_nonzero_subdef xnz nnz xr nr ==>
(x%:num *~ n%:num != 0)
18b
Signed.reality_cond 0
  (mul_reality_subdef xnz nnz xr nr)
  (x%:num *~ n%:num)
  by move: xr nr xnz nnz x n => [[[]|]|] [[[]|]|] [] []// x n;
     rewrite mulrz_neq0//= ?neq0.
18b
18f
move: xr nr xnz nnz x n => [[[]|]|] [[[]|]|] [] []/= x n //;
  do ?[by case: (bottom x)|by case: (bottom n)
      |by rewrite mulrz_ge0|by rewrite mulrz_le0_ge0|by rewrite eq0 mul0rz
      |by rewrite mulrz_ge0_le0|by rewrite mulrz_le0|by rewrite eq0 mulr0z
      |by rewrite -realE rpredMz//; apply: cmp0].
Qed.

Canonical intmul_snum (xnz nnz : nullity) (xr nr : reality)
    (x : {num R & xnz & xr}) (n : {num int & nnz & nr}) :=
  Signed.mk (intmul_snum_subproof x n).

Lemma inv_snum_subproof (xnz : nullity) (xr : reality)
    (x : {num R & xnz & xr}) :
  Signed.spec 0 xnz xr (x%:num^-1 : R).
c7
131
132
133
(xnz ==> ((x%:num^-1 : R) != 0)) &&
Signed.reality_cond 0 xr (x%:num^-1 : R)
Proof.
194
by case: xr x => [[[]|]|]//= [r]/=;
   rewrite invr_eq0 ?(invr_ge0, invr_le0) ?realV.
Qed.

Canonical inv_snum (xnz : nullity) (xr : reality) (x : {num R & xnz & xr}) :=
  Signed.mk (inv_snum_subproof x).

Definition exprn_nonzero_subdef (xnz nnz : nullity)
    (xr nr : reality) : nullity :=
  nz_of_bool (xnz || match nr with Real (Sign =0) => true | _ => false end).
Arguments exprn_nonzero_subdef /.

Definition exprn_reality_subdef (xnz nnz : nullity)
    (xr nr : reality) : reality :=
  match xr, nr with
  | _, Real (Sign =0) => >=0
  | Real (Sign =0), _ => (if nnz then =0 else >=0)%snum_sign
  | Real (Sign >=0), _ => >=0
  | Real _, _ => >=<0
  | _, _ => >?<0
  end.
Arguments exprn_reality_subdef /.

Lemma exprn_snum_subproof (xnz nnz : nullity) (xr nr : reality)
    (x : {num R & xnz & xr}) (n : {compare 0%N & nnz & nr})
    (rnz := exprn_nonzero_subdef xnz nnz xr nr)
    (rrl := exprn_reality_subdef xnz nnz xr nr) :
  Signed.spec 0 rnz rrl (x%:num ^+ n%:num).
c7
16f
170
133
171
rnz:= exprn_nonzero_subdef xnz nnz xr nr: nullity
rrl:= exprn_reality_subdef xnz nnz xr nr: reality
(rnz ==> (x%:num ^+ n%:num != 0)) &&
Signed.reality_cond 0 rrl (x%:num ^+ n%:num)
Proof.
19a
rewrite {}/rnz {}/rrl; apply/andP; split.
179
exprn_nonzero_subdef xnz nnz xr nr ==>
(x%:num ^+ n%:num != 0)
179
Signed.reality_cond 0
  (exprn_reality_subdef xnz nnz xr nr)
  (x%:num ^+ n%:num)
  by move: xr nr xnz nnz x n => [[[]|]|] [[[]|]|] [] []// x n;
    do ?[by case: (bottom x)|by case: (bottom n)];
    rewrite expf_eq0/= ?eq0// ?eq0F ?andbF//.
179
1a7
move: xr nr xnz nnz x n => [[[]|]|] [[[]|]|] [] []/= x [[|n]//= _] //;
  do ?[by case: (bottom x)|by case: (bottom n)|by rewrite [_ || _]realX
      |by rewrite eq0 expr0n|exact: exprn_ge0|by rewrite expr0 ler01].
Qed.

Canonical exprn_snum (xnz nnz : nullity) (xr nr : reality)
    (x : {num R & xnz & xr}) (n : {compare 0%N & nnz & nr}) :=
  Signed.mk (exprn_snum_subproof x n).

Lemma norm_snum_subproof {V : normedZmodType R} (x : V) :
  Signed.spec 0 ?=0 >=0 `|x|.
c7
V: normedZmodType R
x: V
(?=0%snum_nullity ==> (`|x| != 0)) &&
Signed.reality_cond 0 >=0 `|x|
Proof.
1ac by rewrite /=. Qed.

Canonical norm_snum {V : normedZmodType R} (x : V) :=
  Signed.mk (norm_snum_subproof x).

End NumDomainStability.

Section RcfStability.
Context {R : rcfType}.

Definition sqrt_nonzero_subdef (xnz : nullity) (xr : reality) :=
  if xr is Real (Sign >=0) then xnz else MaybeZero.
Arguments sqrt_nonzero_subdef /.

Lemma sqrt_snum_subproof xnz xr (x : {num R & xnz & xr})
    (nz := sqrt_nonzero_subdef xnz xr) :
  Signed.spec 0 nz >=0 (Num.sqrt x%:num).
R: rcfType
131
132
133
nz:= sqrt_nonzero_subdef xnz xr: nullity
(nz ==> (Num.sqrt x%:num != 0)) &&
Signed.reality_cond 0 >=0 (Num.sqrt x%:num)
Proof.
1b4
by rewrite {}/nz; case: xnz xr x => -[[[]|]|]//= x;
   rewrite /= sqrtr_ge0// andbT sqrtr_eq0 le0F.
Qed.

Canonical sqrt_snum xnz xr (x : {num R & xnz & xr}) :=
  Signed.mk (sqrt_snum_subproof x).

End RcfStability.

Section NumClosedStability.
Context {R : numClosedFieldType}.

Definition sqrtC_reality_subdef (xnz : nullity) (xr : reality) : reality :=
  match xr with
  | Real (Sign =0) => =0
  | Real (Sign >=0) => >=0
  | _ => >?<0
  end.
Arguments sqrtC_reality_subdef /.

Lemma sqrtC_snum_subproof xnz xr (x : {num R & xnz & xr})
    (r := sqrtC_reality_subdef xnz xr) :
  Signed.spec 0 xnz r (sqrtC x%:num).
R: numClosedFieldType
131
132
133
r:= sqrtC_reality_subdef xnz xr: reality
(xnz ==> (sqrtC x%:num != 0)) &&
Signed.reality_cond 0 r (sqrtC x%:num)
Proof.
1bc
rewrite {}/r; apply/andP; split.
1bf
131
132
133
xnz ==> (sqrtC x%:num != 0)
1c6
Signed.reality_cond 0 (sqrtC_reality_subdef xnz xr)
  (sqrtC x%:num)
  by rewrite sqrtC_eq0; case: xr xnz x => [[[]|]|] [] /=.
1c6
1ca
by case: xr xnz x => [[[]|]|] []//= x; rewrite ?sqrtC_ge0// sqrtC_eq0 eq0.
Qed.

Canonical sqrtC_snum xnz xr (x : {num R & xnz & xr}) :=
  Signed.mk (sqrtC_snum_subproof x).

End NumClosedStability.

Section NatStability.
Local Open Scope nat_scope.
Implicit Type (n : nat).

Lemma nat_snum_subproof n : Signed.spec 0 ?=0 >=0 n.
n: nat
(?=0%snum_nullity ==> (n != 0)) &&
Signed.reality_cond 0 >=0 n
Proof.
1cf by []. Qed.

Canonical nat_snum n := Signed.mk (nat_snum_subproof n).
Ignoring canonical projection to _ by Signed.r in
nat_snum: redundant with typ_snum
[redundant-canonical-projection,typechecker]

Lemma zeron_snum_subproof : Signed.spec 0 ?=0 =0 0.
(?=0%snum_nullity ==> (0 != 0)) &&
Signed.reality_cond 0 =0 0
Proof.
1d7 by []. Qed.

Canonical zeron_snum := Signed.mk zeron_snum_subproof.

Lemma succn_snum_subproof n : Signed.spec 0 !=0 >=0 n.+1.
1d1
(!=0%snum_nullity ==> (n.+1 != 0)) &&
Signed.reality_cond 0 >=0 n.+1
Proof.
1dc by []. Qed.

Canonical succn_snum n := Signed.mk (succn_snum_subproof n).

Lemma double_snum_subproof nz r (x : {compare 0 & nz & r}) :
  Signed.spec 0 nz r x%:num.*2.
2c
r: reality
x: {compare 0 & nz & r}
(nz ==> ((x%:num).*2 != 0)) &&
Signed.reality_cond 0 r (x%:num).*2
Proof.
1e1 by  move: nz r x => [] [[[]|]|] [[|n]]. Qed.

Canonical double_snum nz r x :=
  Signed.mk (@double_snum_subproof nz r x).

Lemma addn_snum_subproof (xnz ynz : nullity) (xr yr : reality)
    (x : {compare 0 & xnz & xr}) (y : {compare 0 & ynz & yr})
    (rnz := add_nonzero_subdef xnz ynz xr yr)
    (rrl := add_reality_subdef xnz ynz xr yr) :
  Signed.spec 0 rnz rrl (x%:num + y%:num).
d1
d2
x: {compare 0 & xnz & xr}
y: {compare 0 & ynz & yr}
13c
13d
13e
Proof.
1e9
rewrite {}/rnz {}/rrl; apply/andP; split;
by move: xr yr xnz ynz x y => [[[]|]|] [[[]|]|] [] []//= [[|x]//= _] [[|y]].
Qed.

Canonical addn_snum (xnz ynz : nullity) (xr yr : reality)
    (x : {compare 0 & xnz & xr}) (y : {compare 0 & ynz & yr}) :=
  Signed.mk (addn_snum_subproof x y).

Lemma muln_snum_subproof (xnz ynz : nullity) (xr yr : reality)
    (x : {compare 0 & xnz & xr}) (y : {compare 0 & ynz & yr})
    (rnz := mul_nonzero_subdef xnz ynz xr yr)
    (rrl := mul_reality_subdef xnz ynz xr yr) :
  Signed.spec 0 rnz rrl (x%:num * y%:num).
d1
d2
1ec
1ed
15d
15e
15f
Proof.
1f0
rewrite {}/rnz {}/rrl; apply/andP; split;
move: xr yr xnz ynz x y => [[[]|]|] [[[]|]|] [] []//=;
by move=> [[|x]//= _] [[|y]//= _]; rewrite muln0.
Qed.

Canonical muln_snum (xnz ynz : nullity) (xr yr : reality)
    (x : {compare 0 & xnz & xr}) (y : {compare 0 & ynz & yr}) :=
  Signed.mk (muln_snum_subproof x y).

Lemma expn_snum_subproof (xnz nnz : nullity) (xr nr : reality)
    (x : {compare 0 & xnz & xr}) (n : {compare 0 & nnz & nr})
    (rnz := exprn_nonzero_subdef xnz nnz xr nr)
    (rrl := exprn_reality_subdef xnz nnz xr nr) :
  Signed.spec 0 rnz rrl (x%:num ^ n%:num).
16f
170
1ec
n: {compare 0 & nnz & nr}
19d
19e
(rnz ==> (x%:num ^ n%:num != 0)) &&
Signed.reality_cond 0 rrl (x%:num ^ n%:num)
Proof.
1f5
rewrite {}/rnz {}/rrl; apply/andP; split.
16f
170
1ec
1f8
exprn_nonzero_subdef xnz nnz xr nr ==>
(x%:num ^ n%:num != 0)
1fe
Signed.reality_cond 0
  (exprn_reality_subdef xnz nnz xr nr)
  (x%:num ^ n%:num)
  move: xr nr xnz nnz x n => [[[]|]|] [[[]|]|] [] []// x n;
    do ?[by case: (bottom x)|by case: (bottom n)
        |by rewrite ?eq0 ?expn0// expn_eq0 ?eq0F].
1fe
202
move: xr nr xnz nnz x n => [[[]|]|] [[[]|]|] [] []/= x [[|n]//= _] //;
  do ?[by case: (bottom x)|by case: (bottom n)|by rewrite eq0 exp0n].
Qed.

Canonical expn_snum (xnz nnz : nullity) (xr nr : reality)
    (x : {compare 0 & xnz & xr}) (n : {compare 0 & nnz & nr}) :=
  Signed.mk (expn_snum_subproof x n).

Lemma minn_snum_subproof (xnz ynz : nullity) (xr yr : reality)
    (x : {compare 0 & xnz & xr}) (y : {compare 0 & ynz & yr})
    (rnz := min_nonzero_subdef xnz ynz xr yr)
    (rrl := min_reality_subdef xnz ynz xr yr) :
  Signed.spec 0 rnz rrl (min x%:num y%:num).
d1
d2
1ec
1ed
d5
d6
(rnz ==> (Nat.min x%:num y%:num != 0)) &&
Signed.reality_cond 0 rrl (Nat.min x%:num y%:num)
Proof.
207
rewrite {}/rnz {}/rrl; apply/andP; split;
by move: xr yr xnz ynz x y => [[[]|]|] [[[]|]|] [] []//= [[|x]//= _] [[|y]].
Qed.

Canonical minn_snum (xnz ynz : nullity) (xr yr : reality)
    (x : {compare 0 & xnz & xr}) (y : {compare 0 & ynz & yr}) :=
  Signed.mk (minn_snum_subproof x y).

Lemma maxn_snum_subproof (xnz ynz : nullity) (xr yr : reality)
    (x : {compare 0 & xnz & xr}) (y : {compare 0 & ynz & yr})
    (rnz := max_nonzero_subdef xnz ynz xr yr)
    (rrl := max_reality_subdef xnz ynz xr yr) :
  Signed.spec 0 rnz rrl (maxn x%:num y%:num).
d1
d2
1ec
1ed
fe
ff
(rnz ==> (maxn x%:num y%:num != 0)) &&
Signed.reality_cond 0 rrl (maxn x%:num y%:num)
Proof.
20d
rewrite {}/rnz {}/rrl; apply/andP; split;
move: xr yr xnz ynz x y => [[[]|]|] [[[]|]|] [] []//=;
by move=> [[|x]//= _] [[|y]//= _]; rewrite maxnSS.
Qed.

Canonical maxn_snum (xnz ynz : nullity) (xr yr : reality)
    (x : {compare 0 & xnz & xr}) (y : {compare 0 & ynz & yr}) :=
  Signed.mk (maxn_snum_subproof x y).

End NatStability.
Ignoring canonical projection to _ by Signed.r in
nat_snum: redundant with typ_snum
[redundant-canonical-projection,typechecker]

Section Morph0.
Context {R : numDomainType} {cond : reality}.
Local Notation nR := {num R & ?=0 & cond}.
Implicit Types x y : nR.
Local Notation num := (@num _ _ (0 : R) ?=0 cond).

Lemma num_eq0 x : (x%:num == 0) = (x == (widen_signed 0%:sgn : nR)).
c7
2d
x: {num R & ?=0 & cond}
(x%:num == 0) =
(x == (widen_signed 0%:sgn : {num R & ?=0 & cond}))
Proof.
214 by []. Qed.

End Morph0.

Section Morph.
Context {d : unit} {T : porderType d} {x0 : T} {nz : nullity} {cond : reality}.
Local Notation sT := {compare x0 & nz & cond}.
Implicit Types x y : sT.
Local Notation num := (@num _ _ x0 nz cond).

Lemma num_eq : {mono num : x y / x == y}.
e
f
43
2c
2d
{mono num : x y / x == y >-> x == y} Proof.
21b by []. Qed.
Lemma num_le : {mono num : x y / (x <= y)%O}.
21d
{mono num : x y / (x <= y)%O >-> (x <= y)%O} Proof.
221 by []. Qed.
Lemma num_lt : {mono num : x y / (x < y)%O}.
21d
{mono num : x y / (x < y)%O >-> (x < y)%O} Proof.
226 by []. Qed.
Lemma num_min : {morph num : x y / Order.min x y}.
21d
{morph num : x y / Order.min x y >-> Order.min x y}
Proof.
22b by move=> x y; rewrite !minEle num_le -fun_if. Qed.
Lemma num_max : {morph num : x y / Order.max x y}.
21d
{morph num : x y / Order.max x y >-> Order.max x y}
Proof.
230 by move=> x y; rewrite !maxEle num_le -fun_if. Qed.

End Morph.

Section MorphNum.
Context {R : numDomainType} {nz : nullity} {cond : reality}.
Local Notation nR := {num R & nz & cond}.
Implicit Types (a : R) (x y : nR).
Local Notation num := (@num _ _ (0 : R) nz cond).

Lemma num_abs_eq0 a : (`|a|%:nng == 0%:nng) = (a == 0).
c7
2c
2d
a: R
(`|a|%:nng == 0%:nng :> {nonneg R}) = (a == 0)
Proof.
235 by rewrite -normr_eq0. Qed.

End MorphNum.

Section MorphReal.
Context {R : numDomainType} {nz : nullity} {r : real}.
Local Notation nR := {num R & nz & r}.
Implicit Type x y : nR.
Local Notation num := (@num _ _ (0 : R) nz r).

Lemma num_le_maxr a x y :
  a <= Num.max x%:num y%:num = (a <= x%:num) || (a <= y%:num).
c7
2c
c8
238
x, y: {num R & nz & r}
(a <= Num.max x%:num y%:num) =
(a <= x%:num) || (a <= y%:num)
Proof.
23c by rewrite -comparable_le_maxr// real_comparable. Qed.

Lemma num_le_maxl a x y :
  Num.max x%:num  y%:num <= a = (x%:num <= a) && (y%:num <= a).
23e
(Num.max x%:num y%:num <= a) =
(x%:num <= a) && (y%:num <= a)
Proof.
243 by rewrite -comparable_le_maxl// real_comparable. Qed.

Lemma num_le_minr a x y :
  a <= Num.min x%:num y%:num = (a <= x%:num) && (a <= y%:num).
23e
(a <= Num.min x%:num y%:num) =
(a <= x%:num) && (a <= y%:num)
Proof.
248 by rewrite -comparable_le_minr// real_comparable. Qed.

Lemma num_le_minl a x y :
  Num.min x%:num y%:num <= a = (x%:num <= a) || (y%:num <= a).
23e
(Num.min x%:num y%:num <= a) =
(x%:num <= a) || (y%:num <= a)
Proof.
24d by rewrite -comparable_le_minl// real_comparable. Qed.

Lemma num_lt_maxr a x y :
  a < Num.max x%:num y%:num = (a < x%:num) || (a < y%:num).
23e
(a < Num.max x%:num y%:num) =
(a < x%:num) || (a < y%:num)
Proof.
252 by rewrite -comparable_lt_maxr// real_comparable. Qed.

Lemma num_lt_maxl a x y :
  Num.max x%:num  y%:num < a = (x%:num < a) && (y%:num < a).
23e
(Num.max x%:num y%:num < a) =
(x%:num < a) && (y%:num < a)
Proof.
257 by rewrite -comparable_lt_maxl// real_comparable. Qed.

Lemma num_lt_minr a x y :
  a < Num.min x%:num y%:num = (a < x%:num) && (a < y%:num).
23e
(a < Num.min x%:num y%:num) =
(a < x%:num) && (a < y%:num)
Proof.
25c by rewrite -comparable_lt_minr// real_comparable. Qed.

Lemma num_lt_minl a x y :
  Num.min x%:num y%:num < a = (x%:num < a) || (y%:num < a).
23e
(Num.min x%:num y%:num < a) =
(x%:num < a) || (y%:num < a)
Proof.
261 by rewrite -comparable_lt_minl// real_comparable. Qed.

End MorphReal.

Section MorphGe0.
Context {R : numDomainType} {nz : nullity}.
Local Notation nR := {num R & ?=0 & >=0}.
Implicit Type x y : nR.
Local Notation num := (@num _ _ (0 : R) ?=0 >=0).

Lemma num_abs_le a x : 0 <= a -> (`|a|%:nng <= x) = (a <= x%:num).
c7
2c
238
x: {num R & ?=0 & >=0}
0 <= a ->
((`|a|%:nng : {nonneg R}) <= x) = (a <= x%:num)
Proof.
266 by move=> a0; rewrite -num_le//= ger0_norm. Qed.

Lemma num_abs_lt a x : 0 <= a -> (`|a|%:nng < x) = (a < x%:num).
268
0 <= a ->
((`|a|%:nng : {nonneg R}) < x) = (a < x%:num)
Proof.
26d by move=> a0; rewrite -num_lt/= ger0_norm. Qed.
End MorphGe0.

Section Posnum.
Context (R : numDomainType) (x : R) (x_gt0 : 0 < x).
Lemma posnum_subdef : (x != 0) && (0 <= x).
c7
18
x_gt0: 0 < x
(x != 0) && (0 <= x) Proof.
272 by rewrite -lt_def. Qed.
Definition PosNum : {posnum R} := @Signed.mk _ _ 0 !=0 >=0 _ posnum_subdef.
End Posnum.
Definition NngNum (R : numDomainType) (x : R) (x_ge0 : 0 <= x) : {nonneg R} :=
  (@Signed.mk _ _ 0 ?=0 >=0 x x_ge0).

CoInductive posnum_spec (R : numDomainType) (x : R) :
  R -> bool -> bool -> bool -> Type :=
| IsPosnum (p : {posnum R}) : posnum_spec x (p%:num) false true true.

Lemma posnumP (R : numDomainType) (x : R) : 0 < x ->
  posnum_spec x x (x == 0) (0 <= x) (0 < x).
c7
18
0 < x -> posnum_spec x x (x == 0) (0 <= x) (0 < x)
Proof.
279
move=> x_gt0; case: real_ltgt0P (x_gt0) => []; rewrite ?gtr0_real // => _ _.
274
posnum_spec x x false true true
by rewrite -[x]/(PosNum x_gt0)%:num; constructor.
Qed.

CoInductive nonneg_spec (R : numDomainType) (x : R) : R -> bool -> Type :=
| IsNonneg (p : {nonneg R}) : nonneg_spec x (p%:num) true.

Lemma nonnegP (R : numDomainType) (x : R) : 0 <= x -> nonneg_spec x x (0 <= x).
27b
0 <= x -> nonneg_spec x x (0 <= x)
Proof.
283 by move=> xge0; rewrite xge0 -[x]/(NngNum xge0)%:num; constructor. Qed.

(* Section PosnumOrder. *)
(* Variables (R : numDomainType). *)
(* Local Notation nR := {posnum R}. *)

(* Lemma posnum_le_total : totalPOrderMixin [porderType of nR]. *)
(* Proof. by move=> x y; apply: real_comparable. Qed. *)

(* Canonical posnum_latticeType := LatticeType nR posnum_le_total. *)
(* Canonical posnum_distrLatticeType := DistrLatticeType nR posnum_le_total. *)
(* Canonical posnum_orderType := OrderType nR posnum_le_total. *)

(* End PosnumOrder. *)

(* Section NonnegOrder. *)
(* Variables (R : numDomainType). *)
(* Local Notation nR := {nonneg R}. *)

(* Lemma nonneg_le_total : totalPOrderMixin [porderType of nR]. *)
(* Proof. by move=> x y; apply: real_comparable. Qed. *)

(* Canonical nonneg_latticeType := LatticeType nR nonneg_le_total. *)
(* Canonical nonneg_distrLatticeType := DistrLatticeType nR nonneg_le_total. *)
(* Canonical nonneg_orderType := OrderType nR nonneg_le_total. *)

(* End NonnegOrder. *)

(* These proofs help integrate more arithmetic with signed.v. The issue is    *)
(* Terms like `0 < 1-q` with subtraction don't work well. So we hide the      *)
(* subtractions behind `PosNum` and `NngNum` constructors, see sequences.v    *)
(* for examples.                                                              *)
Section onem_signed.
Variable R : numDomainType.
Implicit Types r : R.

Lemma onem_PosNum r (r1 : r < 1) : `1-r = (PosNum (onem_gt0 r1))%:num.
c7
r: R
r1: r < 1
`1-r = (PosNum (onem_gt0 r1))%:num
Proof.
288 by []. Qed.

Lemma onemX_NngNum r (r1 : r <= 1) (r0 : 0 <= r) n :
  `1-(r ^+ n) = (NngNum (onemX_ge0 n r0 r1))%:num.
c7
28b
r1: r <= 1
r0: 0 <= r
1d2
`1-(r ^+ n) = (NngNum (onemX_ge0 n r0 r1))%:num
Proof.
290 by []. Qed.

End onem_signed.