Require Import
  HoTT.Classes.interfaces.abstract_algebra
  HoTT.Classes.theory.additional_operations
  HoTT.Classes.tactics.ring_quote
  HoTT.Classes.theory.rings.
[Loading ML file number_string_notation_plugin.cmxs (using legacy method) ... done]

Generalizable Variables Vlt.

Import Quoting.
Local Set Universe Minimization ToSet.

Section content.
Local Existing Instance almost_ring_semiring.
Local Existing Instance almostring_mor_sr_mor.

Universe UC.
Context {C : Type@{UC} } {V : Type0 }.

Inductive Pol : Type@{UC} :=
  | Pconst (c : C)
  | PX (P : Pol) (v : V) (Q : Pol).

(* [C] is the scalar semiring: Z when working on rings,
   N on semirings, other sometimes. *)
Context `{AlmostRing C} `{DecidablePaths C}.

(* [V] is the type of variables, ie we are defining polynomials [C[V]].
   It has a computable compare so we can normalise polynomials. *)
Context `{Trichotomy@{Set Set Set} V Vlt}.

(* Polynomials are supposed (at the meta level) to be in normal form:
   PX P v Q verifies
     + P <> 0
     + forall w in P, w <= v
     + forall w in Q, w <  v *)

Fixpoint Peqb P Q : Bool :=
  match P, Q with
  | Pconst c, Pconst d => c =? d
  | PX P1 v P2, PX Q1 w Q2 =>
    andb (v =? w) (andb (Peqb P1 Q1) (Peqb P2 Q2))
  | _, _ => false
  end.

Global Instance Peqb_instance : Eqb Pol := Peqb.
Arguments Peqb_instance _ _ /.

Global Instance P0 : canonical_names.Zero Pol := Pconst 0.
Global Instance P1 : canonical_names.One Pol := Pconst 1.

Universe UR.
Context {R : Type@{UR} } `{AlmostRing R}
  (phi : C -> R) `{!AlmostRingPreserving phi}.

Notation Vars V := (V -> R).

Fixpoint eval (vs : Vars V) (P : Pol) : R :=
  match P with
  | Pconst c => phi c
  | PX P v Q =>
    (eval vs P) * (vs v) + (eval vs Q)
  end.

Lemma andb_true : forall a b : Bool, andb a b = true -> a = true /\ b = true.
C: Type
V: Type0
Aplus: canonical_names.Plus C
Amult: canonical_names.Mult C
Azero: canonical_names.Zero C
Aone: canonical_names.One C
Anegate: AlmostNegate C
H: AlmostRing C
H0: DecidablePaths C
Vlt: Relation V
H1: Trichotomy Vlt
R: Type
Aplus0: canonical_names.Plus R
Amult0: canonical_names.Mult R
Azero0: canonical_names.Zero R
Aone0: canonical_names.One R
Anegate0: AlmostNegate R
H2: AlmostRing R
phi: Vars C
AlmostRingPreserving0: AlmostRingPreserving phi
forall a b : Bool,
(a && b)%Bool = true -> ((a = true) * (b = true))%type
Proof.
C: Type
V: Type0
Aplus: canonical_names.Plus C
Amult: canonical_names.Mult C
Azero: canonical_names.Zero C
Aone: canonical_names.One C
Anegate: AlmostNegate C
H: AlmostRing C
H0: DecidablePaths C
Vlt: Relation V
H1: Trichotomy Vlt
R: Type
Aplus0: canonical_names.Plus R
Amult0: canonical_names.Mult R
Azero0: canonical_names.Zero R
Aone0: canonical_names.One R
Anegate0: AlmostNegate R
H2: AlmostRing R
phi: Vars C
AlmostRingPreserving0: AlmostRingPreserving phi
forall a b : Bool,
(a && b)%Bool = true -> ((a = true) * (b = true))%type
intros [|] [|];simpl;auto.
Qed.

Lemma eval_eqb' : forall P Q : Pol, P =? Q = true ->
  forall vs : Vars V, eval vs P = eval vs Q.
C: Type
V: Type0
Aplus: canonical_names.Plus C
Amult: canonical_names.Mult C
Azero: canonical_names.Zero C
Aone: canonical_names.One C
Anegate: AlmostNegate C
H: AlmostRing C
H0: DecidablePaths C
Vlt: Relation V
H1: Trichotomy Vlt
R: Type
Aplus0: canonical_names.Plus R
Amult0: canonical_names.Mult R
Azero0: canonical_names.Zero R
Aone0: canonical_names.One R
Anegate0: AlmostNegate R
H2: AlmostRing R
phi: Vars C
AlmostRingPreserving0: AlmostRingPreserving phi
forall P Q : Pol,
(P =? Q) = true ->
forall vs : Vars V, eval vs P = eval vs Q
Proof.
C: Type
V: Type0
Aplus: canonical_names.Plus C
Amult: canonical_names.Mult C
Azero: canonical_names.Zero C
Aone: canonical_names.One C
Anegate: AlmostNegate C
H: AlmostRing C
H0: DecidablePaths C
Vlt: Relation V
H1: Trichotomy Vlt
R: Type
Aplus0: canonical_names.Plus R
Amult0: canonical_names.Mult R
Azero0: canonical_names.Zero R
Aone0: canonical_names.One R
Anegate0: AlmostNegate R
H2: AlmostRing R
phi: Vars C
AlmostRingPreserving0: AlmostRingPreserving phi
forall P Q : Pol,
(P =? Q) = true ->
forall vs : Vars V, eval vs P = eval vs Q
induction P as [c|P1 IHP1 v P2 IHP2];destruct Q as [d|Q1 w Q2];intros E vs;
change eqb with Peqb in E;simpl in E.
C: Type
V: Type0
Aplus: canonical_names.Plus C
Amult: canonical_names.Mult C
Azero: canonical_names.Zero C
Aone: canonical_names.One C
Anegate: AlmostNegate C
H: AlmostRing C
H0: DecidablePaths C
Vlt: Relation V
H1: Trichotomy Vlt
R: Type
Aplus0: canonical_names.Plus R
Amult0: canonical_names.Mult R
Azero0: canonical_names.Zero R
Aone0: canonical_names.One R
Anegate0: AlmostNegate R
H2: AlmostRing R
phi: Vars C
AlmostRingPreserving0: AlmostRingPreserving phi
c, d: C
E: (c =? d) = true
vs: Vars V
eval vs (Pconst c) = eval vs (Pconst d)
C: Type
V: Type0
Aplus: canonical_names.Plus C
Amult: canonical_names.Mult C
Azero: canonical_names.Zero C
Aone: canonical_names.One C
Anegate: AlmostNegate C
H: AlmostRing C
H0: DecidablePaths C
Vlt: Relation V
H1: Trichotomy Vlt
R: Type
Aplus0: canonical_names.Plus R
Amult0: canonical_names.Mult R
Azero0: canonical_names.Zero R
Aone0: canonical_names.One R
Anegate0: AlmostNegate R
H2: AlmostRing R
phi: Vars C
AlmostRingPreserving0: AlmostRingPreserving phi
c: C
Q1: Pol
w: V
Q2: Pol
E: false = true
vs: Vars V
eval vs (Pconst c) = eval vs (PX Q1 w Q2)
C: Type
V: Type0
Aplus: canonical_names.Plus C
Amult: canonical_names.Mult C
Azero: canonical_names.Zero C
Aone: canonical_names.One C
Anegate: AlmostNegate C
H: AlmostRing C
H0: DecidablePaths C
Vlt: Relation V
H1: Trichotomy Vlt
R: Type
Aplus0: canonical_names.Plus R
Amult0: canonical_names.Mult R
Azero0: canonical_names.Zero R
Aone0: canonical_names.One R
Anegate0: AlmostNegate R
H2: AlmostRing R
phi: Vars C
AlmostRingPreserving0: AlmostRingPreserving phi
P1: Pol
v: V
P2: Pol
IHP1: forall Q : Pol,
(P1 =? Q) = true ->
forall vs : Vars V, eval vs P1 = eval vs Q
IHP2: forall Q : Pol,
(P2 =? Q) = true ->
forall vs : Vars V, eval vs P2 = eval vs Q
d: C
E: false = true
vs: Vars V
eval vs (PX P1 v P2) = eval vs (Pconst d)
C: Type
V: Type0
Aplus: canonical_names.Plus C
Amult: canonical_names.Mult C
Azero: canonical_names.Zero C
Aone: canonical_names.One C
Anegate: AlmostNegate C
H: AlmostRing C
H0: DecidablePaths C
Vlt: Relation V
H1: Trichotomy Vlt
R: Type
Aplus0: canonical_names.Plus R
Amult0: canonical_names.Mult R
Azero0: canonical_names.Zero R
Aone0: canonical_names.One R
Anegate0: AlmostNegate R
H2: AlmostRing R
phi: Vars C
AlmostRingPreserving0: AlmostRingPreserving phi
P1: Pol
v: V
P2: Pol
IHP1: forall Q : Pol,
(P1 =? Q) = true ->
forall vs : Vars V, eval vs P1 = eval vs Q
IHP2: forall Q : Pol,
(P2 =? Q) = true ->
forall vs : Vars V, eval vs P2 = eval vs Q
Q1: Pol
w: V
Q2: Pol
E: ((v =? w) && (Peqb P1 Q1 && Peqb P2 Q2))%Bool =
true
vs: Vars V
eval vs (PX P1 v P2) = eval vs (PX Q1 w Q2)
-
C: Type
V: Type0
Aplus: canonical_names.Plus C
Amult: canonical_names.Mult C
Azero: canonical_names.Zero C
Aone: canonical_names.One C
Anegate: AlmostNegate C
H: AlmostRing C
H0: DecidablePaths C
Vlt: Relation V
H1: Trichotomy Vlt
R: Type
Aplus0: canonical_names.Plus R
Amult0: canonical_names.Mult R
Azero0: canonical_names.Zero R
Aone0: canonical_names.One R
Anegate0: AlmostNegate R
H2: AlmostRing R
phi: Vars C
AlmostRingPreserving0: AlmostRingPreserving phi
c, d: C
E: (c =? d) = true
vs: Vars V
eval vs (Pconst c) = eval vs (Pconst d) simpl.
C: Type
V: Type0
Aplus: canonical_names.Plus C
Amult: canonical_names.Mult C
Azero: canonical_names.Zero C
Aone: canonical_names.One C
Anegate: AlmostNegate C
H: AlmostRing C
H0: DecidablePaths C
Vlt: Relation V
H1: Trichotomy Vlt
R: Type
Aplus0: canonical_names.Plus R
Amult0: canonical_names.Mult R
Azero0: canonical_names.Zero R
Aone0: canonical_names.One R
Anegate0: AlmostNegate R
H2: AlmostRing R
phi: Vars C
AlmostRingPreserving0: AlmostRingPreserving phi
c, d: C
E: (c =? d) = true
vs: Vars V
phi c = phi d apply ap.
C: Type
V: Type0
Aplus: canonical_names.Plus C
Amult: canonical_names.Mult C
Azero: canonical_names.Zero C
Aone: canonical_names.One C
Anegate: AlmostNegate C
H: AlmostRing C
H0: DecidablePaths C
Vlt: Relation V
H1: Trichotomy Vlt
R: Type
Aplus0: canonical_names.Plus R
Amult0: canonical_names.Mult R
Azero0: canonical_names.Zero R
Aone0: canonical_names.One R
Anegate0: AlmostNegate R
H2: AlmostRing R
phi: Vars C
AlmostRingPreserving0: AlmostRingPreserving phi
c, d: C
E: (c =? d) = true
vs: Vars V
c = d apply decide_eqb_ok;trivial.
-
C: Type
V: Type0
Aplus: canonical_names.Plus C
Amult: canonical_names.Mult C
Azero: canonical_names.Zero C
Aone: canonical_names.One C
Anegate: AlmostNegate C
H: AlmostRing C
H0: DecidablePaths C
Vlt: Relation V
H1: Trichotomy Vlt
R: Type
Aplus0: canonical_names.Plus R
Amult0: canonical_names.Mult R
Azero0: canonical_names.Zero R
Aone0: canonical_names.One R
Anegate0: AlmostNegate R
H2: AlmostRing R
phi: Vars C
AlmostRingPreserving0: AlmostRingPreserving phi
c: C
Q1: Pol
w: V
Q2: Pol
E: false = true
vs: Vars V
eval vs (Pconst c) = eval vs (PX Q1 w Q2) destruct (false_ne_true E).
-
C: Type
V: Type0
Aplus: canonical_names.Plus C
Amult: canonical_names.Mult C
Azero: canonical_names.Zero C
Aone: canonical_names.One C
Anegate: AlmostNegate C
H: AlmostRing C
H0: DecidablePaths C
Vlt: Relation V
H1: Trichotomy Vlt
R: Type
Aplus0: canonical_names.Plus R
Amult0: canonical_names.Mult R
Azero0: canonical_names.Zero R
Aone0: canonical_names.One R
Anegate0: AlmostNegate R
H2: AlmostRing R
phi: Vars C
AlmostRingPreserving0: AlmostRingPreserving phi
P1: Pol
v: V
P2: Pol
IHP1: forall Q : Pol,
(P1 =? Q) = true ->
forall vs : Vars V, eval vs P1 = eval vs Q
IHP2: forall Q : Pol,
(P2 =? Q) = true ->
forall vs : Vars V, eval vs P2 = eval vs Q
d: C
E: false = true
vs: Vars V
eval vs (PX P1 v P2) = eval vs (Pconst d) destruct (false_ne_true E).
-
C: Type
V: Type0
Aplus: canonical_names.Plus C
Amult: canonical_names.Mult C
Azero: canonical_names.Zero C
Aone: canonical_names.One C
Anegate: AlmostNegate C
H: AlmostRing C
H0: DecidablePaths C
Vlt: Relation V
H1: Trichotomy Vlt
R: Type
Aplus0: canonical_names.Plus R
Amult0: canonical_names.Mult R
Azero0: canonical_names.Zero R
Aone0: canonical_names.One R
Anegate0: AlmostNegate R
H2: AlmostRing R
phi: Vars C
AlmostRingPreserving0: AlmostRingPreserving phi
P1: Pol
v: V
P2: Pol
IHP1: forall Q : Pol,
(P1 =? Q) = true ->
forall vs : Vars V, eval vs P1 = eval vs Q
IHP2: forall Q : Pol,
(P2 =? Q) = true ->
forall vs : Vars V, eval vs P2 = eval vs Q
Q1: Pol
w: V
Q2: Pol
E: ((v =? w) && (Peqb P1 Q1 && Peqb P2 Q2))%Bool =
true
vs: Vars V
eval vs (PX P1 v P2) = eval vs (PX Q1 w Q2) apply andb_true in E.
C: Type
V: Type0
Aplus: canonical_names.Plus C
Amult: canonical_names.Mult C
Azero: canonical_names.Zero C
Aone: canonical_names.One C
Anegate: AlmostNegate C
H: AlmostRing C
H0: DecidablePaths C
Vlt: Relation V
H1: Trichotomy Vlt
R: Type
Aplus0: canonical_names.Plus R
Amult0: canonical_names.Mult R
Azero0: canonical_names.Zero R
Aone0: canonical_names.One R
Anegate0: AlmostNegate R
H2: AlmostRing R
phi: Vars C
AlmostRingPreserving0: AlmostRingPreserving phi
P1: Pol
v: V
P2: Pol
IHP1: forall Q : Pol,
(P1 =? Q) = true ->
forall vs : Vars V, eval vs P1 = eval vs Q
IHP2: forall Q : Pol,
(P2 =? Q) = true ->
forall vs : Vars V, eval vs P2 = eval vs Q
Q1: Pol
w: V
Q2: Pol
E: (((v =? w) = true) *
 ((Peqb P1 Q1 && Peqb P2 Q2)%Bool = true))%type
vs: Vars V
eval vs (PX P1 v P2) = eval vs (PX Q1 w Q2) destruct E as [E1 E2].
C: Type
V: Type0
Aplus: canonical_names.Plus C
Amult: canonical_names.Mult C
Azero: canonical_names.Zero C
Aone: canonical_names.One C
Anegate: AlmostNegate C
H: AlmostRing C
H0: DecidablePaths C
Vlt: Relation V
H1: Trichotomy Vlt
R: Type
Aplus0: canonical_names.Plus R
Amult0: canonical_names.Mult R
Azero0: canonical_names.Zero R
Aone0: canonical_names.One R
Anegate0: AlmostNegate R
H2: AlmostRing R
phi: Vars C
AlmostRingPreserving0: AlmostRingPreserving phi
P1: Pol
v: V
P2: Pol
IHP1: forall Q : Pol,
(P1 =? Q) = true ->
forall vs : Vars V, eval vs P1 = eval vs Q
IHP2: forall Q : Pol,
(P2 =? Q) = true ->
forall vs : Vars V, eval vs P2 = eval vs Q
Q1: Pol
w: V
Q2: Pol
E1: (v =? w) = true
E2: (Peqb P1 Q1 && Peqb P2 Q2)%Bool = true
vs: Vars V
eval vs (PX P1 v P2) = eval vs (PX Q1 w Q2)
  apply andb_true in E2.
C: Type
V: Type0
Aplus: canonical_names.Plus C
Amult: canonical_names.Mult C
Azero: canonical_names.Zero C
Aone: canonical_names.One C
Anegate: AlmostNegate C
H: AlmostRing C
H0: DecidablePaths C
Vlt: Relation V
H1: Trichotomy Vlt
R: Type
Aplus0: canonical_names.Plus R
Amult0: canonical_names.Mult R
Azero0: canonical_names.Zero R
Aone0: canonical_names.One R
Anegate0: AlmostNegate R
H2: AlmostRing R
phi: Vars C
AlmostRingPreserving0: AlmostRingPreserving phi
P1: Pol
v: V
P2: Pol
IHP1: forall Q : Pol,
(P1 =? Q) = true ->
forall vs : Vars V, eval vs P1 = eval vs Q
IHP2: forall Q : Pol,
(P2 =? Q) = true ->
forall vs : Vars V, eval vs P2 = eval vs Q
Q1: Pol
w: V
Q2: Pol
E1: (v =? w) = true
E2: ((Peqb P1 Q1 = true) * (Peqb P2 Q2 = true))%type
vs: Vars V
eval vs (PX P1 v P2) = eval vs (PX Q1 w Q2) destruct E2 as [E2 E3].
C: Type
V: Type0
Aplus: canonical_names.Plus C
Amult: canonical_names.Mult C
Azero: canonical_names.Zero C
Aone: canonical_names.One C
Anegate: AlmostNegate C
H: AlmostRing C
H0: DecidablePaths C
Vlt: Relation V
H1: Trichotomy Vlt
R: Type
Aplus0: canonical_names.Plus R
Amult0: canonical_names.Mult R
Azero0: canonical_names.Zero R
Aone0: canonical_names.One R
Anegate0: AlmostNegate R
H2: AlmostRing R
phi: Vars C
AlmostRingPreserving0: AlmostRingPreserving phi
P1: Pol
v: V
P2: Pol
IHP1: forall Q : Pol,
(P1 =? Q) = true ->
forall vs : Vars V, eval vs P1 = eval vs Q
IHP2: forall Q : Pol,
(P2 =? Q) = true ->
forall vs : Vars V, eval vs P2 = eval vs Q
Q1: Pol
w: V
Q2: Pol
E1: (v =? w) = true
E2: Peqb P1 Q1 = true
E3: Peqb P2 Q2 = true
vs: Vars V
eval vs (PX P1 v P2) = eval vs (PX Q1 w Q2)
  simpl.
C: Type
V: Type0
Aplus: canonical_names.Plus C
Amult: canonical_names.Mult C
Azero: canonical_names.Zero C
Aone: canonical_names.One C
Anegate: AlmostNegate C
H: AlmostRing C
H0: DecidablePaths C
Vlt: Relation V
H1: Trichotomy Vlt
R: Type
Aplus0: canonical_names.Plus R
Amult0: canonical_names.Mult R
Azero0: canonical_names.Zero R
Aone0: canonical_names.One R
Anegate0: AlmostNegate R
H2: AlmostRing R
phi: Vars C
AlmostRingPreserving0: AlmostRingPreserving phi
P1: Pol
v: V
P2: Pol
IHP1: forall Q : Pol,
(P1 =? Q) = true ->
forall vs : Vars V, eval vs P1 = eval vs Q
IHP2: forall Q : Pol,
(P2 =? Q) = true ->
forall vs : Vars V, eval vs P2 = eval vs Q
Q1: Pol
w: V
Q2: Pol
E1: (v =? w) = true
E2: Peqb P1 Q1 = true
E3: Peqb P2 Q2 = true
vs: Vars V
eval vs P1 * vs v + eval vs P2 =
eval vs Q1 * vs w + eval vs Q2
  apply compare_eqb_eq,tricho_compare_eq in E1.
C: Type
V: Type0
Aplus: canonical_names.Plus C
Amult: canonical_names.Mult C
Azero: canonical_names.Zero C
Aone: canonical_names.One C
Anegate: AlmostNegate C
H: AlmostRing C
H0: DecidablePaths C
Vlt: Relation V
H1: Trichotomy Vlt
R: Type
Aplus0: canonical_names.Plus R
Amult0: canonical_names.Mult R
Azero0: canonical_names.Zero R
Aone0: canonical_names.One R
Anegate0: AlmostNegate R
H2: AlmostRing R
phi: Vars C
AlmostRingPreserving0: AlmostRingPreserving phi
P1: Pol
v: V
P2: Pol
IHP1: forall Q : Pol,
(P1 =? Q) = true ->
forall vs : Vars V, eval vs P1 = eval vs Q
IHP2: forall Q : Pol,
(P2 =? Q) = true ->
forall vs : Vars V, eval vs P2 = eval vs Q
Q1: Pol
w: V
Q2: Pol
E1: v = w
E2: Peqb P1 Q1 = true
E3: Peqb P2 Q2 = true
vs: Vars V
eval vs P1 * vs v + eval vs P2 =
eval vs Q1 * vs w + eval vs Q2
  apply ap011;auto.
C: Type
V: Type0
Aplus: canonical_names.Plus C
Amult: canonical_names.Mult C
Azero: canonical_names.Zero C
Aone: canonical_names.One C
Anegate: AlmostNegate C
H: AlmostRing C
H0: DecidablePaths C
Vlt: Relation V
H1: Trichotomy Vlt
R: Type
Aplus0: canonical_names.Plus R
Amult0: canonical_names.Mult R
Azero0: canonical_names.Zero R
Aone0: canonical_names.One R
Anegate0: AlmostNegate R
H2: AlmostRing R
phi: Vars C
AlmostRingPreserving0: AlmostRingPreserving phi
P1: Pol
v: V
P2: Pol
IHP1: forall Q : Pol,
(P1 =? Q) = true ->
forall vs : Vars V, eval vs P1 = eval vs Q
IHP2: forall Q : Pol,
(P2 =? Q) = true ->
forall vs : Vars V, eval vs P2 = eval vs Q
Q1: Pol
w: V
Q2: Pol
E1: v = w
E2: Peqb P1 Q1 = true
E3: Peqb P2 Q2 = true
vs: Vars V
eval vs P1 * vs v = eval vs Q1 * vs w apply ap011;auto.
Qed.

Definition eval_eqb@{} := ltac:(first [exact eval_eqb'@{Ularge}|
                                       exact eval_eqb']).

Lemma eval_0' : forall P, P =? 0 = true -> forall vs, eval vs P = 0.
C: Type
V: Type0
Aplus: canonical_names.Plus C
Amult: canonical_names.Mult C
Azero: canonical_names.Zero C
Aone: canonical_names.One C
Anegate: AlmostNegate C
H: AlmostRing C
H0: DecidablePaths C
Vlt: Relation V
H1: Trichotomy Vlt
R: Type
Aplus0: canonical_names.Plus R
Amult0: canonical_names.Mult R
Azero0: canonical_names.Zero R
Aone0: canonical_names.One R
Anegate0: AlmostNegate R
H2: AlmostRing R
phi: Vars C
AlmostRingPreserving0: AlmostRingPreserving phi
forall P : Pol,
(P =? 0) = true -> forall vs : Vars V, eval vs P = 0
Proof.
C: Type
V: Type0
Aplus: canonical_names.Plus C
Amult: canonical_names.Mult C
Azero: canonical_names.Zero C
Aone: canonical_names.One C
Anegate: AlmostNegate C
H: AlmostRing C
H0: DecidablePaths C
Vlt: Relation V
H1: Trichotomy Vlt
R: Type
Aplus0: canonical_names.Plus R
Amult0: canonical_names.Mult R
Azero0: canonical_names.Zero R
Aone0: canonical_names.One R
Anegate0: AlmostNegate R
H2: AlmostRing R
phi: Vars C
AlmostRingPreserving0: AlmostRingPreserving phi
forall P : Pol,
(P =? 0) = true -> forall vs : Vars V, eval vs P = 0
induction P;simpl;intros E vs.
C: Type
V: Type0
Aplus: canonical_names.Plus C
Amult: canonical_names.Mult C
Azero: canonical_names.Zero C
Aone: canonical_names.One C
Anegate: AlmostNegate C
H: AlmostRing C
H0: DecidablePaths C
Vlt: Relation V
H1: Trichotomy Vlt
R: Type
Aplus0: canonical_names.Plus R
Amult0: canonical_names.Mult R
Azero0: canonical_names.Zero R
Aone0: canonical_names.One R
Anegate0: AlmostNegate R
H2: AlmostRing R
phi: Vars C
AlmostRingPreserving0: AlmostRingPreserving phi
c: C
E: (Pconst c =? 0) = true
vs: Vars V
phi c = 0
C: Type
V: Type0
Aplus: canonical_names.Plus C
Amult: canonical_names.Mult C
Azero: canonical_names.Zero C
Aone: canonical_names.One C
Anegate: AlmostNegate C
H: AlmostRing C
H0: DecidablePaths C
Vlt: Relation V
H1: Trichotomy Vlt
R: Type
Aplus0: canonical_names.Plus R
Amult0: canonical_names.Mult R
Azero0: canonical_names.Zero R
Aone0: canonical_names.One R
Anegate0: AlmostNegate R
H2: AlmostRing R
phi: Vars C
AlmostRingPreserving0: AlmostRingPreserving phi
P2: Pol
v: V
P3: Pol
IHP1: (P2 =? 0) = true ->
forall vs : Vars V, eval vs P2 = 0
IHP2: (P3 =? 0) = true ->
forall vs : Vars V, eval vs P3 = 0
E: (PX P2 v P3 =? 0) = true
vs: Vars V
eval vs P2 * vs v + eval vs P3 = 0
-
C: Type
V: Type0
Aplus: canonical_names.Plus C
Amult: canonical_names.Mult C
Azero: canonical_names.Zero C
Aone: canonical_names.One C
Anegate: AlmostNegate C
H: AlmostRing C
H0: DecidablePaths C
Vlt: Relation V
H1: Trichotomy Vlt
R: Type
Aplus0: canonical_names.Plus R
Amult0: canonical_names.Mult R
Azero0: canonical_names.Zero R
Aone0: canonical_names.One R
Anegate0: AlmostNegate R
H2: AlmostRing R
phi: Vars C
AlmostRingPreserving0: AlmostRingPreserving phi
c: C
E: (Pconst c =? 0) = true
vs: Vars V
phi c = 0 change eqb with Peqb in E;simpl in E.
C: Type
V: Type0
Aplus: canonical_names.Plus C
Amult: canonical_names.Mult C
Azero: canonical_names.Zero C
Aone: canonical_names.One C
Anegate: AlmostNegate C
H: AlmostRing C
H0: DecidablePaths C
Vlt: Relation V
H1: Trichotomy Vlt
R: Type
Aplus0: canonical_names.Plus R
Amult0: canonical_names.Mult R
Azero0: canonical_names.Zero R
Aone0: canonical_names.One R
Anegate0: AlmostNegate R
H2: AlmostRing R
phi: Vars C
AlmostRingPreserving0: AlmostRingPreserving phi
c: C
E: (c =? 0) = true
vs: Vars V
phi c = 0
  apply decide_eqb_ok in E.
C: Type
V: Type0
Aplus: canonical_names.Plus C
Amult: canonical_names.Mult C
Azero: canonical_names.Zero C
Aone: canonical_names.One C
Anegate: AlmostNegate C
H: AlmostRing C
H0: DecidablePaths C
Vlt: Relation V
H1: Trichotomy Vlt
R: Type
Aplus0: canonical_names.Plus R
Amult0: canonical_names.Mult R
Azero0: canonical_names.Zero R
Aone0: canonical_names.One R
Anegate0: AlmostNegate R
H2: AlmostRing R
phi: Vars C
AlmostRingPreserving0: AlmostRingPreserving phi
c: C
E: c = 0
vs: Vars V
phi c = 0 rewrite E.
C: Type
V: Type0
Aplus: canonical_names.Plus C
Amult: canonical_names.Mult C
Azero: canonical_names.Zero C
Aone: canonical_names.One C
Anegate: AlmostNegate C
H: AlmostRing C
H0: DecidablePaths C
Vlt: Relation V
H1: Trichotomy Vlt
R: Type
Aplus0: canonical_names.Plus R
Amult0: canonical_names.Mult R
Azero0: canonical_names.Zero R
Aone0: canonical_names.One R
Anegate0: AlmostNegate R
H2: AlmostRing R
phi: Vars C
AlmostRingPreserving0: AlmostRingPreserving phi
c: C
E: c = 0
vs: Vars V
phi 0 = 0
  apply preserves_0.
-
C: Type
V: Type0
Aplus: canonical_names.Plus C
Amult: canonical_names.Mult C
Azero: canonical_names.Zero C
Aone: canonical_names.One C
Anegate: AlmostNegate C
H: AlmostRing C
H0: DecidablePaths C
Vlt: Relation V
H1: Trichotomy Vlt
R: Type
Aplus0: canonical_names.Plus R
Amult0: canonical_names.Mult R
Azero0: canonical_names.Zero R
Aone0: canonical_names.One R
Anegate0: AlmostNegate R
H2: AlmostRing R
phi: Vars C
AlmostRingPreserving0: AlmostRingPreserving phi
P2: Pol
v: V
P3: Pol
IHP1: (P2 =? 0) = true ->
forall vs : Vars V, eval vs P2 = 0
IHP2: (P3 =? 0) = true ->
forall vs : Vars V, eval vs P3 = 0
E: (PX P2 v P3 =? 0) = true
vs: Vars V
eval vs P2 * vs v + eval vs P3 = 0 change eqb with Peqb in E;simpl in E.
C: Type
V: Type0
Aplus: canonical_names.Plus C
Amult: canonical_names.Mult C
Azero: canonical_names.Zero C
Aone: canonical_names.One C
Anegate: AlmostNegate C
H: AlmostRing C
H0: DecidablePaths C
Vlt: Relation V
H1: Trichotomy Vlt
R: Type
Aplus0: canonical_names.Plus R
Amult0: canonical_names.Mult R
Azero0: canonical_names.Zero R
Aone0: canonical_names.One R
Anegate0: AlmostNegate R
H2: AlmostRing R
phi: Vars C
AlmostRingPreserving0: AlmostRingPreserving phi
P2: Pol
v: V
P3: Pol
IHP1: (P2 =? 0) = true ->
forall vs : Vars V, eval vs P2 = 0
IHP2: (P3 =? 0) = true ->
forall vs : Vars V, eval vs P3 = 0
E: false = true
vs: Vars V
eval vs P2 * vs v + eval vs P3 = 0
  destruct (false_ne_true E).
Qed.

Definition eval_0@{} := ltac:(first [exact eval_0'@{Ularge}|
                                     exact eval_0']).

Fixpoint addC c P :=
  match P with
  | Pconst d => Pconst (c + d)
  | PX P v Q =>
    PX P v (addC c Q)
  end.

Lemma eval_addC vs : forall c P, eval vs (addC c P) = (phi c) + eval vs P.
C: Type
V: Type0
Aplus: canonical_names.Plus C
Amult: canonical_names.Mult C
Azero: canonical_names.Zero C
Aone: canonical_names.One C
Anegate: AlmostNegate C
H: AlmostRing C
H0: DecidablePaths C
Vlt: Relation V
H1: Trichotomy Vlt
R: Type
Aplus0: canonical_names.Plus R
Amult0: canonical_names.Mult R
Azero0: canonical_names.Zero R
Aone0: canonical_names.One R
Anegate0: AlmostNegate R
H2: AlmostRing R
phi: Vars C
AlmostRingPreserving0: AlmostRingPreserving phi
vs: Vars V
forall (c : C) (P : Pol),
eval vs (addC c P) = phi c + eval vs P
Proof.
C: Type
V: Type0
Aplus: canonical_names.Plus C
Amult: canonical_names.Mult C
Azero: canonical_names.Zero C
Aone: canonical_names.One C
Anegate: AlmostNegate C
H: AlmostRing C
H0: DecidablePaths C
Vlt: Relation V
H1: Trichotomy Vlt
R: Type
Aplus0: canonical_names.Plus R
Amult0: canonical_names.Mult R
Azero0: canonical_names.Zero R
Aone0: canonical_names.One R
Anegate0: AlmostNegate R
H2: AlmostRing R
phi: Vars C
AlmostRingPreserving0: AlmostRingPreserving phi
vs: Vars V
forall (c : C) (P : Pol),
eval vs (addC c P) = phi c + eval vs P
induction P;simpl.
C: Type
V: Type0
Aplus: canonical_names.Plus C
Amult: canonical_names.Mult C
Azero: canonical_names.Zero C
Aone: canonical_names.One C
Anegate: AlmostNegate C
H: AlmostRing C
H0: DecidablePaths C
Vlt: Relation V
H1: Trichotomy Vlt
R: Type
Aplus0: canonical_names.Plus R
Amult0: canonical_names.Mult R
Azero0: canonical_names.Zero R
Aone0: canonical_names.One R
Anegate0: AlmostNegate R
H2: AlmostRing R
phi: Vars C
AlmostRingPreserving0: AlmostRingPreserving phi
vs: Vars V
c, c0: C
phi (c + c0) = phi c + phi c0
C: Type
V: Type0
Aplus: canonical_names.Plus C
Amult: canonical_names.Mult C
Azero: canonical_names.Zero C
Aone: canonical_names.One C
Anegate: AlmostNegate C
H: AlmostRing C
H0: DecidablePaths C
Vlt: Relation V
H1: Trichotomy Vlt
R: Type
Aplus0: canonical_names.Plus R
Amult0: canonical_names.Mult R
Azero0: canonical_names.Zero R
Aone0: canonical_names.One R
Anegate0: AlmostNegate R
H2: AlmostRing R
phi: Vars C
AlmostRingPreserving0: AlmostRingPreserving phi
vs: Vars V
c: C
P2: Pol
v: V
P3: Pol
IHP1: eval vs (addC c P2) = phi c + eval vs P2
IHP2: eval vs (addC c P3) = phi c + eval vs P3
eval vs P2 * vs v + eval vs (addC c P3) =
phi c + (eval vs P2 * vs v + eval vs P3)
-
C: Type
V: Type0
Aplus: canonical_names.Plus C
Amult: canonical_names.Mult C
Azero: canonical_names.Zero C
Aone: canonical_names.One C
Anegate: AlmostNegate C
H: AlmostRing C
H0: DecidablePaths C
Vlt: Relation V
H1: Trichotomy Vlt
R: Type
Aplus0: canonical_names.Plus R
Amult0: canonical_names.Mult R
Azero0: canonical_names.Zero R
Aone0: canonical_names.One R
Anegate0: AlmostNegate R
H2: AlmostRing R
phi: Vars C
AlmostRingPreserving0: AlmostRingPreserving phi
vs: Vars V
c, c0: C
phi (c + c0) = phi c + phi c0 apply preserves_plus.
-
C: Type
V: Type0
Aplus: canonical_names.Plus C
Amult: canonical_names.Mult C
Azero: canonical_names.Zero C
Aone: canonical_names.One C
Anegate: AlmostNegate C
H: AlmostRing C
H0: DecidablePaths C
Vlt: Relation V
H1: Trichotomy Vlt
R: Type
Aplus0: canonical_names.Plus R
Amult0: canonical_names.Mult R
Azero0: canonical_names.Zero R
Aone0: canonical_names.One R
Anegate0: AlmostNegate R
H2: AlmostRing R
phi: Vars C
AlmostRingPreserving0: AlmostRingPreserving phi
vs: Vars V
c: C
P2: Pol
v: V
P3: Pol
IHP1: eval vs (addC c P2) = phi c + eval vs P2
IHP2: eval vs (addC c P3) = phi c + eval vs P3
eval vs P2 * vs v + eval vs (addC c P3) =
phi c + (eval vs P2 * vs v + eval vs P3) rewrite IHP2.
C: Type
V: Type0
Aplus: canonical_names.Plus C
Amult: canonical_names.Mult C
Azero: canonical_names.Zero C
Aone: canonical_names.One C
Anegate: AlmostNegate C
H: AlmostRing C
H0: DecidablePaths C
Vlt: Relation V
H1: Trichotomy Vlt
R: Type
Aplus0: canonical_names.Plus R
Amult0: canonical_names.Mult R
Azero0: canonical_names.Zero R
Aone0: canonical_names.One R
Anegate0: AlmostNegate R
H2: AlmostRing R
phi: Vars C
AlmostRingPreserving0: AlmostRingPreserving phi
vs: Vars V
c: C
P2: Pol
v: V
P3: Pol
IHP1: eval vs (addC c P2) = phi c + eval vs P2
IHP2: eval vs (addC c P3) = phi c + eval vs P3
eval vs P2 * vs v + (phi c + eval vs P3) =
phi c + (eval vs P2 * vs v + eval vs P3)
  rewrite 2!plus_assoc.
C: Type
V: Type0
Aplus: canonical_names.Plus C
Amult: canonical_names.Mult C
Azero: canonical_names.Zero C
Aone: canonical_names.One C
Anegate: AlmostNegate C
H: AlmostRing C
H0: DecidablePaths C
Vlt: Relation V
H1: Trichotomy Vlt
R: Type
Aplus0: canonical_names.Plus R
Amult0: canonical_names.Mult R
Azero0: canonical_names.Zero R
Aone0: canonical_names.One R
Anegate0: AlmostNegate R
H2: AlmostRing R
phi: Vars C
AlmostRingPreserving0: AlmostRingPreserving phi
vs: Vars V
c: C
P2: Pol
v: V
P3: Pol
IHP1: eval vs (addC c P2) = phi c + eval vs P2
IHP2: eval vs (addC c P3) = phi c + eval vs P3
eval vs P2 * vs v + phi c + eval vs P3 =
phi c + eval vs P2 * vs v + eval vs P3 rewrite (plus_comm (phi c)).
C: Type
V: Type0
Aplus: canonical_names.Plus C
Amult: canonical_names.Mult C
Azero: canonical_names.Zero C
Aone: canonical_names.One C
Anegate: AlmostNegate C
H: AlmostRing C
H0: DecidablePaths C
Vlt: Relation V
H1: Trichotomy Vlt
R: Type
Aplus0: canonical_names.Plus R
Amult0: canonical_names.Mult R
Azero0: canonical_names.Zero R
Aone0: canonical_names.One R
Anegate0: AlmostNegate R
H2: AlmostRing R
phi: Vars C
AlmostRingPreserving0: AlmostRingPreserving phi
vs: Vars V
c: C
P2: Pol
v: V
P3: Pol
IHP1: eval vs (addC c P2) = phi c + eval vs P2
IHP2: eval vs (addC c P3) = phi c + eval vs P3
eval vs P2 * vs v + phi c + eval vs P3 =
eval vs P2 * vs v + phi c + eval vs P3
  reflexivity.
Qed.

(* c * v + Q *)
Fixpoint addX' c v Q :=
  match Q with
  | Pconst d => PX (Pconst c) v Q
  | PX Q1 w Q2 =>
    match v ?= w with
    | LT =>
      PX Q1 w (addX' c v Q2)
    | EQ =>
      PX (addC c Q1) v Q2
    | GT => PX (Pconst c) v Q
    end
  end.

Definition addX c v Q := if c =? 0 then Q else addX' c v Q.

Lemma eval_addX'@{} vs : forall c (v:V) Q,
  eval vs (addX' c v Q) = phi c * vs v + eval vs Q.
C: Type
V: Type0
Aplus: canonical_names.Plus C
Amult: canonical_names.Mult C
Azero: canonical_names.Zero C
Aone: canonical_names.One C
Anegate: AlmostNegate C
H: AlmostRing C
H0: DecidablePaths C
Vlt: Relation V
H1: Trichotomy Vlt
R: Type
Aplus0: canonical_names.Plus R
Amult0: canonical_names.Mult R
Azero0: canonical_names.Zero R
Aone0: canonical_names.One R
Anegate0: AlmostNegate R
H2: AlmostRing R
phi: Vars C
AlmostRingPreserving0: AlmostRingPreserving phi
vs: Vars V
forall (c : C) (v : V) (Q : Pol),
eval vs (addX' c v Q) = phi c * vs v + eval vs Q
Proof.
C: Type
V: Type0
Aplus: canonical_names.Plus C
Amult: canonical_names.Mult C
Azero: canonical_names.Zero C
Aone: canonical_names.One C
Anegate: AlmostNegate C
H: AlmostRing C
H0: DecidablePaths C
Vlt: Relation V
H1: Trichotomy Vlt
R: Type
Aplus0: canonical_names.Plus R
Amult0: canonical_names.Mult R
Azero0: canonical_names.Zero R
Aone0: canonical_names.One R
Anegate0: AlmostNegate R
H2: AlmostRing R
phi: Vars C
AlmostRingPreserving0: AlmostRingPreserving phi
vs: Vars V
forall (c : C) (v : V) (Q : Pol),
eval vs (addX' c v Q) = phi c * vs v + eval vs Q
induction Q as [d|Q1 IH1 w Q2 IH2].
C: Type
V: Type0
Aplus: canonical_names.Plus C
Amult: canonical_names.Mult C
Azero: canonical_names.Zero C
Aone: canonical_names.One C
Anegate: AlmostNegate C
H: AlmostRing C
H0: DecidablePaths C
Vlt: Relation V
H1: Trichotomy Vlt
R: Type
Aplus0: canonical_names.Plus R
Amult0: canonical_names.Mult R
Azero0: canonical_names.Zero R
Aone0: canonical_names.One R
Anegate0: AlmostNegate R
H2: AlmostRing R
phi: Vars C
AlmostRingPreserving0: AlmostRingPreserving phi
vs: Vars V
c: C
v: V
d: C
eval vs (addX' c v (Pconst d)) =
phi c * vs v + eval vs (Pconst d)
C: Type
V: Type0
Aplus: canonical_names.Plus C
Amult: canonical_names.Mult C
Azero: canonical_names.Zero C
Aone: canonical_names.One C
Anegate: AlmostNegate C
H: AlmostRing C
H0: DecidablePaths C
Vlt: Relation V
H1: Trichotomy Vlt
R: Type
Aplus0: canonical_names.Plus R
Amult0: canonical_names.Mult R
Azero0: canonical_names.Zero R
Aone0: canonical_names.One R
Anegate0: AlmostNegate R
H2: AlmostRing R
phi: Vars C
AlmostRingPreserving0: AlmostRingPreserving phi
vs: Vars V
c: C
v: V
Q1: Pol
w: V
Q2: Pol
IH1: eval vs (addX' c v Q1) =
phi c * vs v + eval vs Q1
IH2: eval vs (addX' c v Q2) =
phi c * vs v + eval vs Q2
eval vs (addX' c v (PX Q1 w Q2)) =
phi c * vs v + eval vs (PX Q1 w Q2)
-
C: Type
V: Type0
Aplus: canonical_names.Plus C
Amult: canonical_names.Mult C
Azero: canonical_names.Zero C
Aone: canonical_names.One C
Anegate: AlmostNegate C
H: AlmostRing C
H0: DecidablePaths C
Vlt: Relation V
H1: Trichotomy Vlt
R: Type
Aplus0: canonical_names.Plus R
Amult0: canonical_names.Mult R
Azero0: canonical_names.Zero R
Aone0: canonical_names.One R
Anegate0: AlmostNegate R
H2: AlmostRing R
phi: Vars C
AlmostRingPreserving0: AlmostRingPreserving phi
vs: Vars V
c: C
v: V
d: C
eval vs (addX' c v (Pconst d)) =
phi c * vs v + eval vs (Pconst d) simpl.
C: Type
V: Type0
Aplus: canonical_names.Plus C
Amult: canonical_names.Mult C
Azero: canonical_names.Zero C
Aone: canonical_names.One C
Anegate: AlmostNegate C
H: AlmostRing C
H0: DecidablePaths C
Vlt: Relation V
H1: Trichotomy Vlt
R: Type
Aplus0: canonical_names.Plus R
Amult0: canonical_names.Mult R
Azero0: canonical_names.Zero R
Aone0: canonical_names.One R
Anegate0: AlmostNegate R
H2: AlmostRing R
phi: Vars C
AlmostRingPreserving0: AlmostRingPreserving phi
vs: Vars V
c: C
v: V
d: C
phi c * vs v + phi d = phi c * vs v + phi d
  reflexivity.
-
C: Type
V: Type0
Aplus: canonical_names.Plus C
Amult: canonical_names.Mult C
Azero: canonical_names.Zero C
Aone: canonical_names.One C
Anegate: AlmostNegate C
H: AlmostRing C
H0: DecidablePaths C
Vlt: Relation V
H1: Trichotomy Vlt
R: Type
Aplus0: canonical_names.Plus R
Amult0: canonical_names.Mult R
Azero0: canonical_names.Zero R
Aone0: canonical_names.One R
Anegate0: AlmostNegate R
H2: AlmostRing R
phi: Vars C
AlmostRingPreserving0: AlmostRingPreserving phi
vs: Vars V
c: C
v: V
Q1: Pol
w: V
Q2: Pol
IH1: eval vs (addX' c v Q1) =
phi c * vs v + eval vs Q1
IH2: eval vs (addX' c v Q2) =
phi c * vs v + eval vs Q2
eval vs (addX' c v (PX Q1 w Q2)) =
phi c * vs v + eval vs (PX Q1 w Q2) simpl.
C: Type
V: Type0
Aplus: canonical_names.Plus C
Amult: canonical_names.Mult C
Azero: canonical_names.Zero C
Aone: canonical_names.One C
Anegate: AlmostNegate C
H: AlmostRing C
H0: DecidablePaths C
Vlt: Relation V
H1: Trichotomy Vlt
R: Type
Aplus0: canonical_names.Plus R
Amult0: canonical_names.Mult R
Azero0: canonical_names.Zero R
Aone0: canonical_names.One R
Anegate0: AlmostNegate R
H2: AlmostRing R
phi: Vars C
AlmostRingPreserving0: AlmostRingPreserving phi
vs: Vars V
c: C
v: V
Q1: Pol
w: V
Q2: Pol
IH1: eval vs (addX' c v Q1) =
phi c * vs v + eval vs Q1
IH2: eval vs (addX' c v Q2) =
phi c * vs v + eval vs Q2
eval vs
  match v ?= w with
  | LT => PX Q1 w (addX' c v Q2)
  | EQ => PX (addC c Q1) v Q2
  | GT => PX (Pconst c) v (PX Q1 w Q2)
  end =
phi c * vs v + (eval vs Q1 * vs w + eval vs Q2)
  pose proof (tricho_compare_eq v w) as E.
C: Type
V: Type0
Aplus: canonical_names.Plus C
Amult: canonical_names.Mult C
Azero: canonical_names.Zero C
Aone: canonical_names.One C
Anegate: AlmostNegate C
H: AlmostRing C
H0: DecidablePaths C
Vlt: Relation V
H1: Trichotomy Vlt
R: Type
Aplus0: canonical_names.Plus R
Amult0: canonical_names.Mult R
Azero0: canonical_names.Zero R
Aone0: canonical_names.One R
Anegate0: AlmostNegate R
H2: AlmostRing R
phi: Vars C
AlmostRingPreserving0: AlmostRingPreserving phi
vs: Vars V
c: C
v: V
Q1: Pol
w: V
Q2: Pol
IH1: eval vs (addX' c v Q1) =
phi c * vs v + eval vs Q1
IH2: eval vs (addX' c v Q2) =
phi c * vs v + eval vs Q2
E: (v ?= w) = EQ -> v = w
eval vs
  match v ?= w with
  | LT => PX Q1 w (addX' c v Q2)
  | EQ => PX (addC c Q1) v Q2
  | GT => PX (Pconst c) v (PX Q1 w Q2)
  end =
phi c * vs v + (eval vs Q1 * vs w + eval vs Q2)
  destruct (v ?= w);[clear E|rewrite <-E by split;clear E w|clear E].
C: Type
V: Type0
Aplus: canonical_names.Plus C
Amult: canonical_names.Mult C
Azero: canonical_names.Zero C
Aone: canonical_names.One C
Anegate: AlmostNegate C
H: AlmostRing C
H0: DecidablePaths C
Vlt: Relation V
H1: Trichotomy Vlt
R: Type
Aplus0: canonical_names.Plus R
Amult0: canonical_names.Mult R
Azero0: canonical_names.Zero R
Aone0: canonical_names.One R
Anegate0: AlmostNegate R
H2: AlmostRing R
phi: Vars C
AlmostRingPreserving0: AlmostRingPreserving phi
vs: Vars V
c: C
v: V
Q1: Pol
w: V
Q2: Pol
IH1: eval vs (addX' c v Q1) =
phi c * vs v + eval vs Q1
IH2: eval vs (addX' c v Q2) =
phi c * vs v + eval vs Q2
eval vs (PX Q1 w (addX' c v Q2)) =
phi c * vs v + (eval vs Q1 * vs w + eval vs Q2)
C: Type
V: Type0
Aplus: canonical_names.Plus C
Amult: canonical_names.Mult C
Azero: canonical_names.Zero C
Aone: canonical_names.One C
Anegate: AlmostNegate C
H: AlmostRing C
H0: DecidablePaths C
Vlt: Relation V
H1: Trichotomy Vlt
R: Type
Aplus0: canonical_names.Plus R
Amult0: canonical_names.Mult R
Azero0: canonical_names.Zero R
Aone0: canonical_names.One R
Anegate0: AlmostNegate R
H2: AlmostRing R
phi: Vars C
AlmostRingPreserving0: AlmostRingPreserving phi
vs: Vars V
c: C
v: V
Q1, Q2: Pol
IH1: eval vs (addX' c v Q1) =
phi c * vs v + eval vs Q1
IH2: eval vs (addX' c v Q2) =
phi c * vs v + eval vs Q2
eval vs (PX (addC c Q1) v Q2) =
phi c * vs v + (eval vs Q1 * vs v + eval vs Q2)
C: Type
V: Type0
Aplus: canonical_names.Plus C
Amult: canonical_names.Mult C
Azero: canonical_names.Zero C
Aone: canonical_names.One C
Anegate: AlmostNegate C
H: AlmostRing C
H0: DecidablePaths C
Vlt: Relation V
H1: Trichotomy Vlt
R: Type
Aplus0: canonical_names.Plus R
Amult0: canonical_names.Mult R
Azero0: canonical_names.Zero R
Aone0: canonical_names.One R
Anegate0: AlmostNegate R
H2: AlmostRing R
phi: Vars C
AlmostRingPreserving0: AlmostRingPreserving phi
vs: Vars V
c: C
v: V
Q1: Pol
w: V
Q2: Pol
IH1: eval vs (addX' c v Q1) =
phi c * vs v + eval vs Q1
IH2: eval vs (addX' c v Q2) =
phi c * vs v + eval vs Q2
eval vs (PX (Pconst c) v (PX Q1 w Q2)) =
phi c * vs v + (eval vs Q1 * vs w + eval vs Q2)
  +
C: Type
V: Type0
Aplus: canonical_names.Plus C
Amult: canonical_names.Mult C
Azero: canonical_names.Zero C
Aone: canonical_names.One C
Anegate: AlmostNegate C
H: AlmostRing C
H0: DecidablePaths C
Vlt: Relation V
H1: Trichotomy Vlt
R: Type
Aplus0: canonical_names.Plus R
Amult0: canonical_names.Mult R
Azero0: canonical_names.Zero R
Aone0: canonical_names.One R
Anegate0: AlmostNegate R
H2: AlmostRing R
phi: Vars C
AlmostRingPreserving0: AlmostRingPreserving phi
vs: Vars V
c: C
v: V
Q1: Pol
w: V
Q2: Pol
IH1: eval vs (addX' c v Q1) =
phi c * vs v + eval vs Q1
IH2: eval vs (addX' c v Q2) =
phi c * vs v + eval vs Q2
eval vs (PX Q1 w (addX' c v Q2)) =
phi c * vs v + (eval vs Q1 * vs w + eval vs Q2) simpl.
C: Type
V: Type0
Aplus: canonical_names.Plus C
Amult: canonical_names.Mult C
Azero: canonical_names.Zero C
Aone: canonical_names.One C
Anegate: AlmostNegate C
H: AlmostRing C
H0: DecidablePaths C
Vlt: Relation V
H1: Trichotomy Vlt
R: Type
Aplus0: canonical_names.Plus R
Amult0: canonical_names.Mult R
Azero0: canonical_names.Zero R
Aone0: canonical_names.One R
Anegate0: AlmostNegate R
H2: AlmostRing R
phi: Vars C
AlmostRingPreserving0: AlmostRingPreserving phi
vs: Vars V
c: C
v: V
Q1: Pol
w: V
Q2: Pol
IH1: eval vs (addX' c v Q1) =
phi c * vs v + eval vs Q1
IH2: eval vs (addX' c v Q2) =
phi c * vs v + eval vs Q2
eval vs Q1 * vs w + eval vs (addX' c v Q2) =
phi c * vs v + (eval vs Q1 * vs w + eval vs Q2) rewrite IH2.
C: Type
V: Type0
Aplus: canonical_names.Plus C
Amult: canonical_names.Mult C
Azero: canonical_names.Zero C
Aone: canonical_names.One C
Anegate: AlmostNegate C
H: AlmostRing C
H0: DecidablePaths C
Vlt: Relation V
H1: Trichotomy Vlt
R: Type
Aplus0: canonical_names.Plus R
Amult0: canonical_names.Mult R
Azero0: canonical_names.Zero R
Aone0: canonical_names.One R
Anegate0: AlmostNegate R
H2: AlmostRing R
phi: Vars C
AlmostRingPreserving0: AlmostRingPreserving phi
vs: Vars V
c: C
v: V
Q1: Pol
w: V
Q2: Pol
IH1: eval vs (addX' c v Q1) =
phi c * vs v + eval vs Q1
IH2: eval vs (addX' c v Q2) =
phi c * vs v + eval vs Q2
eval vs Q1 * vs w + (phi c * vs v + eval vs Q2) =
phi c * vs v + (eval vs Q1 * vs w + eval vs Q2)
    rewrite 2!plus_assoc.
C: Type
V: Type0
Aplus: canonical_names.Plus C
Amult: canonical_names.Mult C
Azero: canonical_names.Zero C
Aone: canonical_names.One C
Anegate: AlmostNegate C
H: AlmostRing C
H0: DecidablePaths C
Vlt: Relation V
H1: Trichotomy Vlt
R: Type
Aplus0: canonical_names.Plus R
Amult0: canonical_names.Mult R
Azero0: canonical_names.Zero R
Aone0: canonical_names.One R
Anegate0: AlmostNegate R
H2: AlmostRing R
phi: Vars C
AlmostRingPreserving0: AlmostRingPreserving phi
vs: Vars V
c: C
v: V
Q1: Pol
w: V
Q2: Pol
IH1: eval vs (addX' c v Q1) =
phi c * vs v + eval vs Q1
IH2: eval vs (addX' c v Q2) =
phi c * vs v + eval vs Q2
eval vs Q1 * vs w + phi c * vs v + eval vs Q2 =
phi c * vs v + eval vs Q1 * vs w + eval vs Q2 apply ap011;trivial.
C: Type
V: Type0
Aplus: canonical_names.Plus C
Amult: canonical_names.Mult C
Azero: canonical_names.Zero C
Aone: canonical_names.One C
Anegate: AlmostNegate C
H: AlmostRing C
H0: DecidablePaths C
Vlt: Relation V
H1: Trichotomy Vlt
R: Type
Aplus0: canonical_names.Plus R
Amult0: canonical_names.Mult R
Azero0: canonical_names.Zero R
Aone0: canonical_names.One R
Anegate0: AlmostNegate R
H2: AlmostRing R
phi: Vars C
AlmostRingPreserving0: AlmostRingPreserving phi
vs: Vars V
c: C
v: V
Q1: Pol
w: V
Q2: Pol
IH1: eval vs (addX' c v Q1) =
phi c * vs v + eval vs Q1
IH2: eval vs (addX' c v Q2) =
phi c * vs v + eval vs Q2
eval vs Q1 * vs w + phi c * vs v =
phi c * vs v + eval vs Q1 * vs w
    apply plus_comm.
  +
C: Type
V: Type0
Aplus: canonical_names.Plus C
Amult: canonical_names.Mult C
Azero: canonical_names.Zero C
Aone: canonical_names.One C
Anegate: AlmostNegate C
H: AlmostRing C
H0: DecidablePaths C
Vlt: Relation V
H1: Trichotomy Vlt
R: Type
Aplus0: canonical_names.Plus R
Amult0: canonical_names.Mult R
Azero0: canonical_names.Zero R
Aone0: canonical_names.One R
Anegate0: AlmostNegate R
H2: AlmostRing R
phi: Vars C
AlmostRingPreserving0: AlmostRingPreserving phi
vs: Vars V
c: C
v: V
Q1, Q2: Pol
IH1: eval vs (addX' c v Q1) =
phi c * vs v + eval vs Q1
IH2: eval vs (addX' c v Q2) =
phi c * vs v + eval vs Q2
eval vs (PX (addC c Q1) v Q2) =
phi c * vs v + (eval vs Q1 * vs v + eval vs Q2) simpl.
C: Type
V: Type0
Aplus: canonical_names.Plus C
Amult: canonical_names.Mult C
Azero: canonical_names.Zero C
Aone: canonical_names.One C
Anegate: AlmostNegate C
H: AlmostRing C
H0: DecidablePaths C
Vlt: Relation V
H1: Trichotomy Vlt
R: Type
Aplus0: canonical_names.Plus R
Amult0: canonical_names.Mult R
Azero0: canonical_names.Zero R
Aone0: canonical_names.One R
Anegate0: AlmostNegate R
H2: AlmostRing R
phi: Vars C
AlmostRingPreserving0: AlmostRingPreserving phi
vs: Vars V
c: C
v: V
Q1, Q2: Pol
IH1: eval vs (addX' c v Q1) =
phi c * vs v + eval vs Q1
IH2: eval vs (addX' c v Q2) =
phi c * vs v + eval vs Q2
eval vs (addC c Q1) * vs v + eval vs Q2 =
phi c * vs v + (eval vs Q1 * vs v + eval vs Q2) rewrite eval_addC.
C: Type
V: Type0
Aplus: canonical_names.Plus C
Amult: canonical_names.Mult C
Azero: canonical_names.Zero C
Aone: canonical_names.One C
Anegate: AlmostNegate C
H: AlmostRing C
H0: DecidablePaths C
Vlt: Relation V
H1: Trichotomy Vlt
R: Type
Aplus0: canonical_names.Plus R
Amult0: canonical_names.Mult R
Azero0: canonical_names.Zero R
Aone0: canonical_names.One R
Anegate0: AlmostNegate R
H2: AlmostRing R
phi: Vars C
AlmostRingPreserving0: AlmostRingPreserving phi
vs: Vars V
c: C
v: V
Q1, Q2: Pol
IH1: eval vs (addX' c v Q1) =
phi c * vs v + eval vs Q1
IH2: eval vs (addX' c v Q2) =
phi c * vs v + eval vs Q2
(phi c + eval vs Q1) * vs v + eval vs Q2 =
phi c * vs v + (eval vs Q1 * vs v + eval vs Q2)
    rewrite plus_mult_distr_r.
C: Type
V: Type0
Aplus: canonical_names.Plus C
Amult: canonical_names.Mult C
Azero: canonical_names.Zero C
Aone: canonical_names.One C
Anegate: AlmostNegate C
H: AlmostRing C
H0: DecidablePaths C
Vlt: Relation V
H1: Trichotomy Vlt
R: Type
Aplus0: canonical_names.Plus R
Amult0: canonical_names.Mult R
Azero0: canonical_names.Zero R
Aone0: canonical_names.One R
Anegate0: AlmostNegate R
H2: AlmostRing R
phi: Vars C
AlmostRingPreserving0: AlmostRingPreserving phi
vs: Vars V
c: C
v: V
Q1, Q2: Pol
IH1: eval vs (addX' c v Q1) =
phi c * vs v + eval vs Q1
IH2: eval vs (addX' c v Q2) =
phi c * vs v + eval vs Q2
phi c * vs v + eval vs Q1 * vs v + eval vs Q2 =
phi c * vs v + (eval vs Q1 * vs v + eval vs Q2)
    symmetry;apply plus_assoc.
  +
C: Type
V: Type0
Aplus: canonical_names.Plus C
Amult: canonical_names.Mult C
Azero: canonical_names.Zero C
Aone: canonical_names.One C
Anegate: AlmostNegate C
H: AlmostRing C
H0: DecidablePaths C
Vlt: Relation V
H1: Trichotomy Vlt
R: Type
Aplus0: canonical_names.Plus R
Amult0: canonical_names.Mult R
Azero0: canonical_names.Zero R
Aone0: canonical_names.One R
Anegate0: AlmostNegate R
H2: AlmostRing R
phi: Vars C
AlmostRingPreserving0: AlmostRingPreserving phi
vs: Vars V
c: C
v: V
Q1: Pol
w: V
Q2: Pol
IH1: eval vs (addX' c v Q1) =
phi c * vs v + eval vs Q1
IH2: eval vs (addX' c v Q2) =
phi c * vs v + eval vs Q2
eval vs (PX (Pconst c) v (PX Q1 w Q2)) =
phi c * vs v + (eval vs Q1 * vs w + eval vs Q2) simpl.
C: Type
V: Type0
Aplus: canonical_names.Plus C
Amult: canonical_names.Mult C
Azero: canonical_names.Zero C
Aone: canonical_names.One C
Anegate: AlmostNegate C
H: AlmostRing C
H0: DecidablePaths C
Vlt: Relation V
H1: Trichotomy Vlt
R: Type
Aplus0: canonical_names.Plus R
Amult0: canonical_names.Mult R
Azero0: canonical_names.Zero R
Aone0: canonical_names.One R
Anegate0: AlmostNegate R
H2: AlmostRing R
phi: Vars C
AlmostRingPreserving0: AlmostRingPreserving phi
vs: Vars V
c: C
v: V
Q1: Pol
w: V
Q2: Pol
IH1: eval vs (addX' c v Q1) =
phi c * vs v + eval vs Q1
IH2: eval vs (addX' c v Q2) =
phi c * vs v + eval vs Q2
phi c * vs v + (eval vs Q1 * vs w + eval vs Q2) =
phi c * vs v + (eval vs Q1 * vs w + eval vs Q2) reflexivity.
Qed.

Lemma eval_addX vs : forall c (v:V) Q,
  eval vs (addX c v Q) = phi c * vs v + eval vs Q.
C: Type
V: Type0
Aplus: canonical_names.Plus C
Amult: canonical_names.Mult C
Azero: canonical_names.Zero C
Aone: canonical_names.One C
Anegate: AlmostNegate C
H: AlmostRing C
H0: DecidablePaths C
Vlt: Relation V
H1: Trichotomy Vlt
R: Type
Aplus0: canonical_names.Plus R
Amult0: canonical_names.Mult R
Azero0: canonical_names.Zero R
Aone0: canonical_names.One R
Anegate0: AlmostNegate R
H2: AlmostRing R
phi: Vars C
AlmostRingPreserving0: AlmostRingPreserving phi
vs: Vars V
forall (c : C) (v : V) (Q : Pol),
eval vs (addX c v Q) = phi c * vs v + eval vs Q
Proof.
C: Type
V: Type0
Aplus: canonical_names.Plus C
Amult: canonical_names.Mult C
Azero: canonical_names.Zero C
Aone: canonical_names.One C
Anegate: AlmostNegate C
H: AlmostRing C
H0: DecidablePaths C
Vlt: Relation V
H1: Trichotomy Vlt
R: Type
Aplus0: canonical_names.Plus R
Amult0: canonical_names.Mult R
Azero0: canonical_names.Zero R
Aone0: canonical_names.One R
Anegate0: AlmostNegate R
H2: AlmostRing R
phi: Vars C
AlmostRingPreserving0: AlmostRingPreserving phi
vs: Vars V
forall (c : C) (v : V) (Q : Pol),
eval vs (addX c v Q) = phi c * vs v + eval vs Q
intros.
C: Type
V: Type0
Aplus: canonical_names.Plus C
Amult: canonical_names.Mult C
Azero: canonical_names.Zero C
Aone: canonical_names.One C
Anegate: AlmostNegate C
H: AlmostRing C
H0: DecidablePaths C
Vlt: Relation V
H1: Trichotomy Vlt
R: Type
Aplus0: canonical_names.Plus R
Amult0: canonical_names.Mult R
Azero0: canonical_names.Zero R
Aone0: canonical_names.One R
Anegate0: AlmostNegate R
H2: AlmostRing R
phi: Vars C
AlmostRingPreserving0: AlmostRingPreserving phi
vs: Vars V
c: C
v: V
Q: Pol
eval vs (addX c v Q) = phi c * vs v + eval vs Q unfold addX.
C: Type
V: Type0
Aplus: canonical_names.Plus C
Amult: canonical_names.Mult C
Azero: canonical_names.Zero C
Aone: canonical_names.One C
Anegate: AlmostNegate C
H: AlmostRing C
H0: DecidablePaths C
Vlt: Relation V
H1: Trichotomy Vlt
R: Type
Aplus0: canonical_names.Plus R
Amult0: canonical_names.Mult R
Azero0: canonical_names.Zero R
Aone0: canonical_names.One R
Anegate0: AlmostNegate R
H2: AlmostRing R
phi: Vars C
AlmostRingPreserving0: AlmostRingPreserving phi
vs: Vars V
c: C
v: V
Q: Pol
eval vs (if c =? 0 then Q else addX' c v Q) =
phi c * vs v + eval vs Q
pose proof (decide_eqb_ok c 0) as E.
C: Type
V: Type0
Aplus: canonical_names.Plus C
Amult: canonical_names.Mult C
Azero: canonical_names.Zero C
Aone: canonical_names.One C
Anegate: AlmostNegate C
H: AlmostRing C
H0: DecidablePaths C
Vlt: Relation V
H1: Trichotomy Vlt
R: Type
Aplus0: canonical_names.Plus R
Amult0: canonical_names.Mult R
Azero0: canonical_names.Zero R
Aone0: canonical_names.One R
Anegate0: AlmostNegate R
H2: AlmostRing R
phi: Vars C
AlmostRingPreserving0: AlmostRingPreserving phi
vs: Vars V
c: C
v: V
Q: Pol
E: (c =? 0) = true <-> c = 0
eval vs (if c =? 0 then Q else addX' c v Q) =
phi c * vs v + eval vs Q
destruct (c =? 0).
C: Type
V: Type0
Aplus: canonical_names.Plus C
Amult: canonical_names.Mult C
Azero: canonical_names.Zero C
Aone: canonical_names.One C
Anegate: AlmostNegate C
H: AlmostRing C
H0: DecidablePaths C
Vlt: Relation V
H1: Trichotomy Vlt
R: Type
Aplus0: canonical_names.Plus R
Amult0: canonical_names.Mult R
Azero0: canonical_names.Zero R
Aone0: canonical_names.One R
Anegate0: AlmostNegate R
H2: AlmostRing R
phi: Vars C
AlmostRingPreserving0: AlmostRingPreserving phi
vs: Vars V
c: C
v: V
Q: Pol
E: true = true <-> c = 0
eval vs Q = phi c * vs v + eval vs Q
C: Type
V: Type0
Aplus: canonical_names.Plus C
Amult: canonical_names.Mult C
Azero: canonical_names.Zero C
Aone: canonical_names.One C
Anegate: AlmostNegate C
H: AlmostRing C
H0: DecidablePaths C
Vlt: Relation V
H1: Trichotomy Vlt
R: Type
Aplus0: canonical_names.Plus R
Amult0: canonical_names.Mult R
Azero0: canonical_names.Zero R
Aone0: canonical_names.One R
Anegate0: AlmostNegate R
H2: AlmostRing R
phi: Vars C
AlmostRingPreserving0: AlmostRingPreserving phi
vs: Vars V
c: C
v: V
Q: Pol
E: false = true <-> c = 0
eval vs (addX' c v Q) = phi c * vs v + eval vs Q
-
C: Type
V: Type0
Aplus: canonical_names.Plus C
Amult: canonical_names.Mult C
Azero: canonical_names.Zero C
Aone: canonical_names.One C
Anegate: AlmostNegate C
H: AlmostRing C
H0: DecidablePaths C
Vlt: Relation V
H1: Trichotomy Vlt
R: Type
Aplus0: canonical_names.Plus R
Amult0: canonical_names.Mult R
Azero0: canonical_names.Zero R
Aone0: canonical_names.One R
Anegate0: AlmostNegate R
H2: AlmostRing R
phi: Vars C
AlmostRingPreserving0: AlmostRingPreserving phi
vs: Vars V
c: C
v: V
Q: Pol
E: true = true <-> c = 0
eval vs Q = phi c * vs v + eval vs Q rewrite (fst E) by split.
C: Type
V: Type0
Aplus: canonical_names.Plus C
Amult: canonical_names.Mult C
Azero: canonical_names.Zero C
Aone: canonical_names.One C
Anegate: AlmostNegate C
H: AlmostRing C
H0: DecidablePaths C
Vlt: Relation V
H1: Trichotomy Vlt
R: Type
Aplus0: canonical_names.Plus R
Amult0: canonical_names.Mult R
Azero0: canonical_names.Zero R
Aone0: canonical_names.One R
Anegate0: AlmostNegate R
H2: AlmostRing R
phi: Vars C
AlmostRingPreserving0: AlmostRingPreserving phi
vs: Vars V
c: C
v: V
Q: Pol
E: true = true <-> c = 0
eval vs Q = phi 0 * vs v + eval vs Q rewrite (preserves_0 (f:=phi)).
C: Type
V: Type0
Aplus: canonical_names.Plus C
Amult: canonical_names.Mult C
Azero: canonical_names.Zero C
Aone: canonical_names.One C
Anegate: AlmostNegate C
H: AlmostRing C
H0: DecidablePaths C
Vlt: Relation V
H1: Trichotomy Vlt
R: Type
Aplus0: canonical_names.Plus R
Amult0: canonical_names.Mult R
Azero0: canonical_names.Zero R
Aone0: canonical_names.One R
Anegate0: AlmostNegate R
H2: AlmostRing R
phi: Vars C
AlmostRingPreserving0: AlmostRingPreserving phi
vs: Vars V
c: C
v: V
Q: Pol
E: true = true <-> c = 0
eval vs Q = 0 * vs v + eval vs Q
  rewrite mult_0_l,plus_0_l.
C: Type
V: Type0
Aplus: canonical_names.Plus C
Amult: canonical_names.Mult C
Azero: canonical_names.Zero C
Aone: canonical_names.One C
Anegate: AlmostNegate C
H: AlmostRing C
H0: DecidablePaths C
Vlt: Relation V
H1: Trichotomy Vlt
R: Type
Aplus0: canonical_names.Plus R
Amult0: canonical_names.Mult R
Azero0: canonical_names.Zero R
Aone0: canonical_names.One R
Anegate0: AlmostNegate R
H2: AlmostRing R
phi: Vars C
AlmostRingPreserving0: AlmostRingPreserving phi
vs: Vars V
c: C
v: V
Q: Pol
E: true = true <-> c = 0
eval vs Q = eval vs Q split.
-
C: Type
V: Type0
Aplus: canonical_names.Plus C
Amult: canonical_names.Mult C
Azero: canonical_names.Zero C
Aone: canonical_names.One C
Anegate: AlmostNegate C
H: AlmostRing C
H0: DecidablePaths C
Vlt: Relation V
H1: Trichotomy Vlt
R: Type
Aplus0: canonical_names.Plus R
Amult0: canonical_names.Mult R
Azero0: canonical_names.Zero R
Aone0: canonical_names.One R
Anegate0: AlmostNegate R
H2: AlmostRing R
phi: Vars C
AlmostRingPreserving0: AlmostRingPreserving phi
vs: Vars V
c: C
v: V
Q: Pol
E: false = true <-> c = 0
eval vs (addX' c v Q) = phi c * vs v + eval vs Q apply eval_addX'.
Qed.

Definition PXguard@{} P v Q := if eqb P 0 then Q else PX P v Q.

Lemma eval_PXguard vs : forall P (v:V) Q,
  eval vs (PXguard P v Q) = eval vs P * vs v + eval vs Q.
C: Type
V: Type0
Aplus: canonical_names.Plus C
Amult: canonical_names.Mult C
Azero: canonical_names.Zero C
Aone: canonical_names.One C
Anegate: AlmostNegate C
H: AlmostRing C
H0: DecidablePaths C
Vlt: Relation V
H1: Trichotomy Vlt
R: Type
Aplus0: canonical_names.Plus R
Amult0: canonical_names.Mult R
Azero0: canonical_names.Zero R
Aone0: canonical_names.One R
Anegate0: AlmostNegate R
H2: AlmostRing R
phi: Vars C
AlmostRingPreserving0: AlmostRingPreserving phi
vs: Vars V
forall (P : Pol) (v : V) (Q : Pol),
eval vs (PXguard P v Q) = eval vs P * vs v + eval vs Q
Proof.
C: Type
V: Type0
Aplus: canonical_names.Plus C
Amult: canonical_names.Mult C
Azero: canonical_names.Zero C
Aone: canonical_names.One C
Anegate: AlmostNegate C
H: AlmostRing C
H0: DecidablePaths C
Vlt: Relation V
H1: Trichotomy Vlt
R: Type
Aplus0: canonical_names.Plus R
Amult0: canonical_names.Mult R
Azero0: canonical_names.Zero R
Aone0: canonical_names.One R
Anegate0: AlmostNegate R
H2: AlmostRing R
phi: Vars C
AlmostRingPreserving0: AlmostRingPreserving phi
vs: Vars V
forall (P : Pol) (v : V) (Q : Pol),
eval vs (PXguard P v Q) = eval vs P * vs v + eval vs Q
intros.
C: Type
V: Type0
Aplus: canonical_names.Plus C
Amult: canonical_names.Mult C
Azero: canonical_names.Zero C
Aone: canonical_names.One C
Anegate: AlmostNegate C
H: AlmostRing C
H0: DecidablePaths C
Vlt: Relation V
H1: Trichotomy Vlt
R: Type
Aplus0: canonical_names.Plus R
Amult0: canonical_names.Mult R
Azero0: canonical_names.Zero R
Aone0: canonical_names.One R
Anegate0: AlmostNegate R
H2: AlmostRing R
phi: Vars C
AlmostRingPreserving0: AlmostRingPreserving phi
vs: Vars V
P: Pol
v: V
Q: Pol
eval vs (PXguard P v Q) = eval vs P * vs v + eval vs Q unfold PXguard.
C: Type
V: Type0
Aplus: canonical_names.Plus C
Amult: canonical_names.Mult C
Azero: canonical_names.Zero C
Aone: canonical_names.One C
Anegate: AlmostNegate C
H: AlmostRing C
H0: DecidablePaths C
Vlt: Relation V
H1: Trichotomy Vlt
R: Type
Aplus0: canonical_names.Plus R
Amult0: canonical_names.Mult R
Azero0: canonical_names.Zero R
Aone0: canonical_names.One R
Anegate0: AlmostNegate R
H2: AlmostRing R
phi: Vars C
AlmostRingPreserving0: AlmostRingPreserving phi
vs: Vars V
P: Pol
v: V
Q: Pol
eval vs (if P =? 0 then Q else PX P v Q) =
eval vs P * vs v + eval vs Q
pose proof (eval_0 P) as E.
C: Type
V: Type0
Aplus: canonical_names.Plus C
Amult: canonical_names.Mult C
Azero: canonical_names.Zero C
Aone: canonical_names.One C
Anegate: AlmostNegate C
H: AlmostRing C
H0: DecidablePaths C
Vlt: Relation V
H1: Trichotomy Vlt
R: Type
Aplus0: canonical_names.Plus R
Amult0: canonical_names.Mult R
Azero0: canonical_names.Zero R
Aone0: canonical_names.One R
Anegate0: AlmostNegate R
H2: AlmostRing R
phi: Vars C
AlmostRingPreserving0: AlmostRingPreserving phi
vs: Vars V
P: Pol
v: V
Q: Pol
E: (P =? 0) = true ->
forall vs : Vars V, eval vs P = 0
eval vs (if P =? 0 then Q else PX P v Q) =
eval vs P * vs v + eval vs Q
destruct (P =? 0).
C: Type
V: Type0
Aplus: canonical_names.Plus C
Amult: canonical_names.Mult C
Azero: canonical_names.Zero C
Aone: canonical_names.One C
Anegate: AlmostNegate C
H: AlmostRing C
H0: DecidablePaths C
Vlt: Relation V
H1: Trichotomy Vlt
R: Type
Aplus0: canonical_names.Plus R
Amult0: canonical_names.Mult R
Azero0: canonical_names.Zero R
Aone0: canonical_names.One R
Anegate0: AlmostNegate R
H2: AlmostRing R
phi: Vars C
AlmostRingPreserving0: AlmostRingPreserving phi
vs: Vars V
P: Pol
v: V
Q: Pol
E: true = true -> forall vs : Vars V, eval vs P = 0
eval vs Q = eval vs P * vs v + eval vs Q
C: Type
V: Type0
Aplus: canonical_names.Plus C
Amult: canonical_names.Mult C
Azero: canonical_names.Zero C
Aone: canonical_names.One C
Anegate: AlmostNegate C
H: AlmostRing C
H0: DecidablePaths C
Vlt: Relation V
H1: Trichotomy Vlt
R: Type
Aplus0: canonical_names.Plus R
Amult0: canonical_names.Mult R
Azero0: canonical_names.Zero R
Aone0: canonical_names.One R
Anegate0: AlmostNegate R
H2: AlmostRing R
phi: Vars C
AlmostRingPreserving0: AlmostRingPreserving phi
vs: Vars V
P: Pol
v: V
Q: Pol
E: false = true -> forall vs : Vars V, eval vs P = 0
eval vs (PX P v Q) = eval vs P * vs v + eval vs Q
-
C: Type
V: Type0
Aplus: canonical_names.Plus C
Amult: canonical_names.Mult C
Azero: canonical_names.Zero C
Aone: canonical_names.One C
Anegate: AlmostNegate C
H: AlmostRing C
H0: DecidablePaths C
Vlt: Relation V
H1: Trichotomy Vlt
R: Type
Aplus0: canonical_names.Plus R
Amult0: canonical_names.Mult R
Azero0: canonical_names.Zero R
Aone0: canonical_names.One R
Anegate0: AlmostNegate R
H2: AlmostRing R
phi: Vars C
AlmostRingPreserving0: AlmostRingPreserving phi
vs: Vars V
P: Pol
v: V
Q: Pol
E: true = true -> forall vs : Vars V, eval vs P = 0
eval vs Q = eval vs P * vs v + eval vs Q rewrite E by split.
C: Type
V: Type0
Aplus: canonical_names.Plus C
Amult: canonical_names.Mult C
Azero: canonical_names.Zero C
Aone: canonical_names.One C
Anegate: AlmostNegate C
H: AlmostRing C
H0: DecidablePaths C
Vlt: Relation V
H1: Trichotomy Vlt
R: Type
Aplus0: canonical_names.Plus R
Amult0: canonical_names.Mult R
Azero0: canonical_names.Zero R
Aone0: canonical_names.One R
Anegate0: AlmostNegate R
H2: AlmostRing R
phi: Vars C
AlmostRingPreserving0: AlmostRingPreserving phi
vs: Vars V
P: Pol
v: V
Q: Pol
E: true = true -> forall vs : Vars V, eval vs P = 0
eval vs Q = 0 * vs v + eval vs Q
  rewrite mult_0_l,plus_0_l.
C: Type
V: Type0
Aplus: canonical_names.Plus C
Amult: canonical_names.Mult C
Azero: canonical_names.Zero C
Aone: canonical_names.One C
Anegate: AlmostNegate C
H: AlmostRing C
H0: DecidablePaths C
Vlt: Relation V
H1: Trichotomy Vlt
R: Type
Aplus0: canonical_names.Plus R
Amult0: canonical_names.Mult R
Azero0: canonical_names.Zero R
Aone0: canonical_names.One R
Anegate0: AlmostNegate R
H2: AlmostRing R
phi: Vars C
AlmostRingPreserving0: AlmostRingPreserving phi
vs: Vars V
P: Pol
v: V
Q: Pol
E: true = true -> forall vs : Vars V, eval vs P = 0
eval vs Q = eval vs Q split.
-
C: Type
V: Type0
Aplus: canonical_names.Plus C
Amult: canonical_names.Mult C
Azero: canonical_names.Zero C
Aone: canonical_names.One C
Anegate: AlmostNegate C
H: AlmostRing C
H0: DecidablePaths C
Vlt: Relation V
H1: Trichotomy Vlt
R: Type
Aplus0: canonical_names.Plus R
Amult0: canonical_names.Mult R
Azero0: canonical_names.Zero R
Aone0: canonical_names.One R
Anegate0: AlmostNegate R
H2: AlmostRing R
phi: Vars C
AlmostRingPreserving0: AlmostRingPreserving phi
vs: Vars V
P: Pol
v: V
Q: Pol
E: false = true -> forall vs : Vars V, eval vs P = 0
eval vs (PX P v Q) = eval vs P * vs v + eval vs Q reflexivity.
Qed.

Fixpoint mulC c P :=
  match P with
  | Pconst d => Pconst (c * d)
  | PX P v Q =>
    (* in some semirings we can have zero divisors, so P' might be zero *)
    PXguard (mulC c P) v (mulC c Q)
  end.

Lemma eval_mulC vs : forall c P, eval vs (mulC c P) = (phi c) * eval vs P.
C: Type
V: Type0
Aplus: canonical_names.Plus C
Amult: canonical_names.Mult C
Azero: canonical_names.Zero C
Aone: canonical_names.One C
Anegate: AlmostNegate C
H: AlmostRing C
H0: DecidablePaths C
Vlt: Relation V
H1: Trichotomy Vlt
R: Type
Aplus0: canonical_names.Plus R
Amult0: canonical_names.Mult R
Azero0: canonical_names.Zero R
Aone0: canonical_names.One R
Anegate0: AlmostNegate R
H2: AlmostRing R
phi: Vars C
AlmostRingPreserving0: AlmostRingPreserving phi
vs: Vars V
forall (c : C) (P : Pol),
eval vs (mulC c P) = phi c * eval vs P
Proof.
C: Type
V: Type0
Aplus: canonical_names.Plus C
Amult: canonical_names.Mult C
Azero: canonical_names.Zero C
Aone: canonical_names.One C
Anegate: AlmostNegate C
H: AlmostRing C
H0: DecidablePaths C
Vlt: Relation V
H1: Trichotomy Vlt
R: Type
Aplus0: canonical_names.Plus R
Amult0: canonical_names.Mult R
Azero0: canonical_names.Zero R
Aone0: canonical_names.One R
Anegate0: AlmostNegate R
H2: AlmostRing R
phi: Vars C
AlmostRingPreserving0: AlmostRingPreserving phi
vs: Vars V
forall (c : C) (P : Pol),
eval vs (mulC c P) = phi c * eval vs P
induction P as [d | P1 IH1 v P2 IH2];simpl.
C: Type
V: Type0
Aplus: canonical_names.Plus C
Amult: canonical_names.Mult C
Azero: canonical_names.Zero C
Aone: canonical_names.One C
Anegate: AlmostNegate C
H: AlmostRing C
H0: DecidablePaths C
Vlt: Relation V
H1: Trichotomy Vlt
R: Type
Aplus0: canonical_names.Plus R
Amult0: canonical_names.Mult R
Azero0: canonical_names.Zero R
Aone0: canonical_names.One R
Anegate0: AlmostNegate R
H2: AlmostRing R
phi: Vars C
AlmostRingPreserving0: AlmostRingPreserving phi
vs: Vars V
c, d: C
phi (c * d) = phi c * phi d
C: Type
V: Type0
Aplus: canonical_names.Plus C
Amult: canonical_names.Mult C
Azero: canonical_names.Zero C
Aone: canonical_names.One C
Anegate: AlmostNegate C
H: AlmostRing C
H0: DecidablePaths C
Vlt: Relation V
H1: Trichotomy Vlt
R: Type
Aplus0: canonical_names.Plus R
Amult0: canonical_names.Mult R
Azero0: canonical_names.Zero R
Aone0: canonical_names.One R
Anegate0: AlmostNegate R
H2: AlmostRing R
phi: Vars C
AlmostRingPreserving0: AlmostRingPreserving phi
vs: Vars V
c: C
P1: Pol
v: V
P2: Pol
IH1: eval vs (mulC c P1) = phi c * eval vs P1
IH2: eval vs (mulC c P2) = phi c * eval vs P2
eval vs (PXguard (mulC c P1) v (mulC c P2)) =
phi c * (eval vs P1 * vs v + eval vs P2)
-
C: Type
V: Type0
Aplus: canonical_names.Plus C
Amult: canonical_names.Mult C
Azero: canonical_names.Zero C
Aone: canonical_names.One C
Anegate: AlmostNegate C
H: AlmostRing C
H0: DecidablePaths C
Vlt: Relation V
H1: Trichotomy Vlt
R: Type
Aplus0: canonical_names.Plus R
Amult0: canonical_names.Mult R
Azero0: canonical_names.Zero R
Aone0: canonical_names.One R
Anegate0: AlmostNegate R
H2: AlmostRing R
phi: Vars C
AlmostRingPreserving0: AlmostRingPreserving phi
vs: Vars V
c, d: C
phi (c * d) = phi c * phi d apply preserves_mult.
-
C: Type
V: Type0
Aplus: canonical_names.Plus C
Amult: canonical_names.Mult C
Azero: canonical_names.Zero C
Aone: canonical_names.One C
Anegate: AlmostNegate C
H: AlmostRing C
H0: DecidablePaths C
Vlt: Relation V
H1: Trichotomy Vlt
R: Type
Aplus0: canonical_names.Plus R
Amult0: canonical_names.Mult R
Azero0: canonical_names.Zero R
Aone0: canonical_names.One R
Anegate0: AlmostNegate R
H2: AlmostRing R
phi: Vars C
AlmostRingPreserving0: AlmostRingPreserving phi
vs: Vars V
c: C
P1: Pol
v: V
P2: Pol
IH1: eval vs (mulC c P1) = phi c * eval vs P1
IH2: eval vs (mulC c P2) = phi c * eval vs P2
eval vs (PXguard (mulC c P1) v (mulC c P2)) =
phi c * (eval vs P1 * vs v + eval vs P2) rewrite eval_PXguard.
C: Type
V: Type0
Aplus: canonical_names.Plus C
Amult: canonical_names.Mult C
Azero: canonical_names.Zero C
Aone: canonical_names.One C
Anegate: AlmostNegate C
H: AlmostRing C
H0: DecidablePaths C
Vlt: Relation V
H1: Trichotomy Vlt
R: Type
Aplus0: canonical_names.Plus R
Amult0: canonical_names.Mult R
Azero0: canonical_names.Zero R
Aone0: canonical_names.One R
Anegate0: AlmostNegate R
H2: AlmostRing R
phi: Vars C
AlmostRingPreserving0: AlmostRingPreserving phi
vs: Vars V
c: C
P1: Pol
v: V
P2: Pol
IH1: eval vs (mulC c P1) = phi c * eval vs P1
IH2: eval vs (mulC c P2) = phi c * eval vs P2
eval vs (mulC c P1) * vs v + eval vs (mulC c P2) =
phi c * (eval vs P1 * vs v + eval vs P2)
  rewrite IH1,IH2,plus_mult_distr_l,mult_assoc.
C: Type
V: Type0
Aplus: canonical_names.Plus C
Amult: canonical_names.Mult C
Azero: canonical_names.Zero C
Aone: canonical_names.One C
Anegate: AlmostNegate C
H: AlmostRing C
H0: DecidablePaths C
Vlt: Relation V
H1: Trichotomy Vlt
R: Type
Aplus0: canonical_names.Plus R
Amult0: canonical_names.Mult R
Azero0: canonical_names.Zero R
Aone0: canonical_names.One R
Anegate0: AlmostNegate R
H2: AlmostRing R
phi: Vars C
AlmostRingPreserving0: AlmostRingPreserving phi
vs: Vars V
c: C
P1: Pol
v: V
P2: Pol
IH1: eval vs (mulC c P1) = phi c * eval vs P1
IH2: eval vs (mulC c P2) = phi c * eval vs P2
phi c * eval vs P1 * vs v + phi c * eval vs P2 =
phi c * eval vs P1 * vs v + phi c * eval vs P2 reflexivity.
Qed.

(* if P <= v, P <> 0, and addP Q = P + Q then P * v + Q *)
Fixpoint add_aux addP P v Q :=
  match Q with
  | Pconst _ => PX P v Q
  | PX Q1 w Q2 =>
    match v ?= w with
    | LT =>
      PX Q1 w (add_aux addP P v Q2)
    | EQ => PXguard (addP Q1) v Q2
    | GT =>
      PX P v Q
    end
  end.

Fixpoint add P Q :=
  match P with
  | Pconst c => addC c Q
  | PX P1 v P2 => add_aux (add P1) P1 v (add P2 Q)
  end.

Lemma eval_add_aux vs P addP
  (Eadd : forall Q, eval vs (addP Q) = eval vs P + eval vs Q)
  : forall (v:V) Q, eval vs (add_aux addP P v Q) = eval vs P * vs v + eval vs Q.
C: Type
V: Type0
Aplus: canonical_names.Plus C
Amult: canonical_names.Mult C
Azero: canonical_names.Zero C
Aone: canonical_names.One C
Anegate: AlmostNegate C
H: AlmostRing C
H0: DecidablePaths C
Vlt: Relation V
H1: Trichotomy Vlt
R: Type
Aplus0: canonical_names.Plus R
Amult0: canonical_names.Mult R
Azero0: canonical_names.Zero R
Aone0: canonical_names.One R
Anegate0: AlmostNegate R
H2: AlmostRing R
phi: Vars C
AlmostRingPreserving0: AlmostRingPreserving phi
vs: Vars V
P: Pol
addP: Pol -> Pol
Eadd: forall Q : Pol,
eval vs (addP Q) = eval vs P + eval vs Q
forall (v : V) (Q : Pol),
eval vs (add_aux addP P v Q) =
eval vs P * vs v + eval vs Q
Proof.
C: Type
V: Type0
Aplus: canonical_names.Plus C
Amult: canonical_names.Mult C
Azero: canonical_names.Zero C
Aone: canonical_names.One C
Anegate: AlmostNegate C
H: AlmostRing C
H0: DecidablePaths C
Vlt: Relation V
H1: Trichotomy Vlt
R: Type
Aplus0: canonical_names.Plus R
Amult0: canonical_names.Mult R
Azero0: canonical_names.Zero R
Aone0: canonical_names.One R
Anegate0: AlmostNegate R
H2: AlmostRing R
phi: Vars C
AlmostRingPreserving0: AlmostRingPreserving phi
vs: Vars V
P: Pol
addP: Pol -> Pol
Eadd: forall Q : Pol,
eval vs (addP Q) = eval vs P + eval vs Q
forall (v : V) (Q : Pol),
eval vs (add_aux addP P v Q) =
eval vs P * vs v + eval vs Q
induction Q as [d|Q1 IH1 w Q2 IH2].
C: Type
V: Type0
Aplus: canonical_names.Plus C
Amult: canonical_names.Mult C
Azero: canonical_names.Zero C
Aone: canonical_names.One C
Anegate: AlmostNegate C
H: AlmostRing C
H0: DecidablePaths C
Vlt: Relation V
H1: Trichotomy Vlt
R: Type
Aplus0: canonical_names.Plus R
Amult0: canonical_names.Mult R
Azero0: canonical_names.Zero R
Aone0: canonical_names.One R
Anegate0: AlmostNegate R
H2: AlmostRing R
phi: Vars C
AlmostRingPreserving0: AlmostRingPreserving phi
vs: Vars V
P: Pol
addP: Pol -> Pol
Eadd: forall Q : Pol,
eval vs (addP Q) = eval vs P + eval vs Q
v: V
d: C
eval vs (add_aux addP P v (Pconst d)) =
eval vs P * vs v + eval vs (Pconst d)
C: Type
V: Type0
Aplus: canonical_names.Plus C
Amult: canonical_names.Mult C
Azero: canonical_names.Zero C
Aone: canonical_names.One C
Anegate: AlmostNegate C
H: AlmostRing C
H0: DecidablePaths C
Vlt: Relation V
H1: Trichotomy Vlt
R: Type
Aplus0: canonical_names.Plus R
Amult0: canonical_names.Mult R
Azero0: canonical_names.Zero R
Aone0: canonical_names.One R
Anegate0: AlmostNegate R
H2: AlmostRing R
phi: Vars C
AlmostRingPreserving0: AlmostRingPreserving phi
vs: Vars V
P: Pol
addP: Pol -> Pol
Eadd: forall Q : Pol,
eval vs (addP Q) = eval vs P + eval vs Q
v: V
Q1: Pol
w: V
Q2: Pol
IH1: eval vs (add_aux addP P v Q1) =
eval vs P * vs v + eval vs Q1
IH2: eval vs (add_aux addP P v Q2) =
eval vs P * vs v + eval vs Q2
eval vs (add_aux addP P v (PX Q1 w Q2)) =
eval vs P * vs v + eval vs (PX Q1 w Q2)
-
C: Type
V: Type0
Aplus: canonical_names.Plus C
Amult: canonical_names.Mult C
Azero: canonical_names.Zero C
Aone: canonical_names.One C
Anegate: AlmostNegate C
H: AlmostRing C
H0: DecidablePaths C
Vlt: Relation V
H1: Trichotomy Vlt
R: Type
Aplus0: canonical_names.Plus R
Amult0: canonical_names.Mult R
Azero0: canonical_names.Zero R
Aone0: canonical_names.One R
Anegate0: AlmostNegate R
H2: AlmostRing R
phi: Vars C
AlmostRingPreserving0: AlmostRingPreserving phi
vs: Vars V
P: Pol
addP: Pol -> Pol
Eadd: forall Q : Pol,
eval vs (addP Q) = eval vs P + eval vs Q
v: V
d: C
eval vs (add_aux addP P v (Pconst d)) =
eval vs P * vs v + eval vs (Pconst d) simpl.
C: Type
V: Type0
Aplus: canonical_names.Plus C
Amult: canonical_names.Mult C
Azero: canonical_names.Zero C
Aone: canonical_names.One C
Anegate: AlmostNegate C
H: AlmostRing C
H0: DecidablePaths C
Vlt: Relation V
H1: Trichotomy Vlt
R: Type
Aplus0: canonical_names.Plus R
Amult0: canonical_names.Mult R
Azero0: canonical_names.Zero R
Aone0: canonical_names.One R
Anegate0: AlmostNegate R
H2: AlmostRing R
phi: Vars C
AlmostRingPreserving0: AlmostRingPreserving phi
vs: Vars V
P: Pol
addP: Pol -> Pol
Eadd: forall Q : Pol,
eval vs (addP Q) = eval vs P + eval vs Q
v: V
d: C
eval vs P * vs v + phi d = eval vs P * vs v + phi d reflexivity.
-
C: Type
V: Type0
Aplus: canonical_names.Plus C
Amult: canonical_names.Mult C
Azero: canonical_names.Zero C
Aone: canonical_names.One C
Anegate: AlmostNegate C
H: AlmostRing C
H0: DecidablePaths C
Vlt: Relation V
H1: Trichotomy Vlt
R: Type
Aplus0: canonical_names.Plus R
Amult0: canonical_names.Mult R
Azero0: canonical_names.Zero R
Aone0: canonical_names.One R
Anegate0: AlmostNegate R
H2: AlmostRing R
phi: Vars C
AlmostRingPreserving0: AlmostRingPreserving phi
vs: Vars V
P: Pol
addP: Pol -> Pol
Eadd: forall Q : Pol,
eval vs (addP Q) = eval vs P + eval vs Q
v: V
Q1: Pol
w: V
Q2: Pol
IH1: eval vs (add_aux addP P v Q1) =
eval vs P * vs v + eval vs Q1
IH2: eval vs (add_aux addP P v Q2) =
eval vs P * vs v + eval vs Q2
eval vs (add_aux addP P v (PX Q1 w Q2)) =
eval vs P * vs v + eval vs (PX Q1 w Q2) simpl.
C: Type
V: Type0
Aplus: canonical_names.Plus C
Amult: canonical_names.Mult C
Azero: canonical_names.Zero C
Aone: canonical_names.One C
Anegate: AlmostNegate C
H: AlmostRing C
H0: DecidablePaths C
Vlt: Relation V
H1: Trichotomy Vlt
R: Type
Aplus0: canonical_names.Plus R
Amult0: canonical_names.Mult R
Azero0: canonical_names.Zero R
Aone0: canonical_names.One R
Anegate0: AlmostNegate R
H2: AlmostRing R
phi: Vars C
AlmostRingPreserving0: AlmostRingPreserving phi
vs: Vars V
P: Pol
addP: Pol -> Pol
Eadd: forall Q : Pol,
eval vs (addP Q) = eval vs P + eval vs Q
v: V
Q1: Pol
w: V
Q2: Pol
IH1: eval vs (add_aux addP P v Q1) =
eval vs P * vs v + eval vs Q1
IH2: eval vs (add_aux addP P v Q2) =
eval vs P * vs v + eval vs Q2
eval vs
  match v ?= w with
  | LT => PX Q1 w (add_aux addP P v Q2)
  | EQ => PXguard (addP Q1) v Q2
  | GT => PX P v (PX Q1 w Q2)
  end =
eval vs P * vs v + (eval vs Q1 * vs w + eval vs Q2)
  pose proof (tricho_compare_eq v w) as E.
C: Type
V: Type0
Aplus: canonical_names.Plus C
Amult: canonical_names.Mult C
Azero: canonical_names.Zero C
Aone: canonical_names.One C
Anegate: AlmostNegate C
H: AlmostRing C
H0: DecidablePaths C
Vlt: Relation V
H1: Trichotomy Vlt
R: Type
Aplus0: canonical_names.Plus R
Amult0: canonical_names.Mult R
Azero0: canonical_names.Zero R
Aone0: canonical_names.One R
Anegate0: AlmostNegate R
H2: AlmostRing R
phi: Vars C
AlmostRingPreserving0: AlmostRingPreserving phi
vs: Vars V
P: Pol
addP: Pol -> Pol
Eadd: forall Q : Pol,
eval vs (addP Q) = eval vs P + eval vs Q
v: V
Q1: Pol
w: V
Q2: Pol
IH1: eval vs (add_aux addP P v Q1) =
eval vs P * vs v + eval vs Q1
IH2: eval vs (add_aux addP P v Q2) =
eval vs P * vs v + eval vs Q2
E: (v ?= w) = EQ -> v = w
eval vs
  match v ?= w with
  | LT => PX Q1 w (add_aux addP P v Q2)
  | EQ => PXguard (addP Q1) v Q2
  | GT => PX P v (PX Q1 w Q2)
  end =
eval vs P * vs v + (eval vs Q1 * vs w + eval vs Q2)
  destruct (v ?= w);[clear E|rewrite <-E by split;clear E w|clear E].
C: Type
V: Type0
Aplus: canonical_names.Plus C
Amult: canonical_names.Mult C
Azero: canonical_names.Zero C
Aone: canonical_names.One C
Anegate: AlmostNegate C
H: AlmostRing C
H0: DecidablePaths C
Vlt: Relation V
H1: Trichotomy Vlt
R: Type
Aplus0: canonical_names.Plus R
Amult0: canonical_names.Mult R
Azero0: canonical_names.Zero R
Aone0: canonical_names.One R
Anegate0: AlmostNegate R
H2: AlmostRing R
phi: Vars C
AlmostRingPreserving0: AlmostRingPreserving phi
vs: Vars V
P: Pol
addP: Pol -> Pol
Eadd: forall Q : Pol,
eval vs (addP Q) = eval vs P + eval vs Q
v: V
Q1: Pol
w: V
Q2: Pol
IH1: eval vs (add_aux addP P v Q1) =
eval vs P * vs v + eval vs Q1
IH2: eval vs (add_aux addP P v Q2) =
eval vs P * vs v + eval vs Q2
eval vs (PX Q1 w (add_aux addP P v Q2)) =
eval vs P * vs v + (eval vs Q1 * vs w + eval vs Q2)
C: Type
V: Type0
Aplus: canonical_names.Plus C
Amult: canonical_names.Mult C
Azero: canonical_names.Zero C
Aone: canonical_names.One C
Anegate: AlmostNegate C
H: AlmostRing C
H0: DecidablePaths C
Vlt: Relation V
H1: Trichotomy Vlt
R: Type
Aplus0: canonical_names.Plus R
Amult0: canonical_names.Mult R
Azero0: canonical_names.Zero R
Aone0: canonical_names.One R
Anegate0: AlmostNegate R
H2: AlmostRing R
phi: Vars C
AlmostRingPreserving0: AlmostRingPreserving phi
vs: Vars V
P: Pol
addP: Pol -> Pol
Eadd: forall Q : Pol,
eval vs (addP Q) = eval vs P + eval vs Q
v: V
Q1, Q2: Pol
IH1: eval vs (add_aux addP P v Q1) =
eval vs P * vs v + eval vs Q1
IH2: eval vs (add_aux addP P v Q2) =
eval vs P * vs v + eval vs Q2
eval vs (PXguard (addP Q1) v Q2) =
eval vs P * vs v + (eval vs Q1 * vs v + eval vs Q2)
C: Type
V: Type0
Aplus: canonical_names.Plus C
Amult: canonical_names.Mult C
Azero: canonical_names.Zero C
Aone: canonical_names.One C
Anegate: AlmostNegate C
H: AlmostRing C
H0: DecidablePaths C
Vlt: Relation V
H1: Trichotomy Vlt
R: Type
Aplus0: canonical_names.Plus R
Amult0: canonical_names.Mult R
Azero0: canonical_names.Zero R
Aone0: canonical_names.One R
Anegate0: AlmostNegate R
H2: AlmostRing R
phi: Vars C
AlmostRingPreserving0: AlmostRingPreserving phi
vs: Vars V
P: Pol
addP: Pol -> Pol
Eadd: forall Q : Pol,
eval vs (addP Q) = eval vs P + eval vs Q
v: V
Q1: Pol
w: V
Q2: Pol
IH1: eval vs (add_aux addP P v Q1) =
eval vs P * vs v + eval vs Q1
IH2: eval vs (add_aux addP P v Q2) =
eval vs P * vs v + eval vs Q2
eval vs (PX P v (PX Q1 w Q2)) =
eval vs P * vs v + (eval vs Q1 * vs w + eval vs Q2)
  +
C: Type
V: Type0
Aplus: canonical_names.Plus C
Amult: canonical_names.Mult C
Azero: canonical_names.Zero C
Aone: canonical_names.One C
Anegate: AlmostNegate C
H: AlmostRing C
H0: DecidablePaths C
Vlt: Relation V
H1: Trichotomy Vlt
R: Type
Aplus0: canonical_names.Plus R
Amult0: canonical_names.Mult R
Azero0: canonical_names.Zero R
Aone0: canonical_names.One R
Anegate0: AlmostNegate R
H2: AlmostRing R
phi: Vars C
AlmostRingPreserving0: AlmostRingPreserving phi
vs: Vars V
P: Pol
addP: Pol -> Pol
Eadd: forall Q : Pol,
eval vs (addP Q) = eval vs P + eval vs Q
v: V
Q1: Pol
w: V
Q2: Pol
IH1: eval vs (add_aux addP P v Q1) =
eval vs P * vs v + eval vs Q1
IH2: eval vs (add_aux addP P v Q2) =
eval vs P * vs v + eval vs Q2
eval vs (PX Q1 w (add_aux addP P v Q2)) =
eval vs P * vs v + (eval vs Q1 * vs w + eval vs Q2) simpl.
C: Type
V: Type0
Aplus: canonical_names.Plus C
Amult: canonical_names.Mult C
Azero: canonical_names.Zero C
Aone: canonical_names.One C
Anegate: AlmostNegate C
H: AlmostRing C
H0: DecidablePaths C
Vlt: Relation V
H1: Trichotomy Vlt
R: Type
Aplus0: canonical_names.Plus R
Amult0: canonical_names.Mult R
Azero0: canonical_names.Zero R
Aone0: canonical_names.One R
Anegate0: AlmostNegate R
H2: AlmostRing R
phi: Vars C
AlmostRingPreserving0: AlmostRingPreserving phi
vs: Vars V
P: Pol
addP: Pol -> Pol
Eadd: forall Q : Pol,
eval vs (addP Q) = eval vs P + eval vs Q
v: V
Q1: Pol
w: V
Q2: Pol
IH1: eval vs (add_aux addP P v Q1) =
eval vs P * vs v + eval vs Q1
IH2: eval vs (add_aux addP P v Q2) =
eval vs P * vs v + eval vs Q2
eval vs Q1 * vs w + eval vs (add_aux addP P v Q2) =
eval vs P * vs v + (eval vs Q1 * vs w + eval vs Q2)
    rewrite IH2.
C: Type
V: Type0
Aplus: canonical_names.Plus C
Amult: canonical_names.Mult C
Azero: canonical_names.Zero C
Aone: canonical_names.One C
Anegate: AlmostNegate C
H: AlmostRing C
H0: DecidablePaths C
Vlt: Relation V
H1: Trichotomy Vlt
R: Type
Aplus0: canonical_names.Plus R
Amult0: canonical_names.Mult R
Azero0: canonical_names.Zero R
Aone0: canonical_names.One R
Anegate0: AlmostNegate R
H2: AlmostRing R
phi: Vars C
AlmostRingPreserving0: AlmostRingPreserving phi
vs: Vars V
P: Pol
addP: Pol -> Pol
Eadd: forall Q : Pol,
eval vs (addP Q) = eval vs P + eval vs Q
v: V
Q1: Pol
w: V
Q2: Pol
IH1: eval vs (add_aux addP P v Q1) =
eval vs P * vs v + eval vs Q1
IH2: eval vs (add_aux addP P v Q2) =
eval vs P * vs v + eval vs Q2
eval vs Q1 * vs w + (eval vs P * vs v + eval vs Q2) =
eval vs P * vs v + (eval vs Q1 * vs w + eval vs Q2)
    rewrite 2!plus_assoc.
C: Type
V: Type0
Aplus: canonical_names.Plus C
Amult: canonical_names.Mult C
Azero: canonical_names.Zero C
Aone: canonical_names.One C
Anegate: AlmostNegate C
H: AlmostRing C
H0: DecidablePaths C
Vlt: Relation V
H1: Trichotomy Vlt
R: Type
Aplus0: canonical_names.Plus R
Amult0: canonical_names.Mult R
Azero0: canonical_names.Zero R
Aone0: canonical_names.One R
Anegate0: AlmostNegate R
H2: AlmostRing R
phi: Vars C
AlmostRingPreserving0: AlmostRingPreserving phi
vs: Vars V
P: Pol
addP: Pol -> Pol
Eadd: forall Q : Pol,
eval vs (addP Q) = eval vs P + eval vs Q
v: V
Q1: Pol
w: V
Q2: Pol
IH1: eval vs (add_aux addP P v Q1) =
eval vs P * vs v + eval vs Q1
IH2: eval vs (add_aux addP P v Q2) =
eval vs P * vs v + eval vs Q2
eval vs Q1 * vs w + eval vs P * vs v + eval vs Q2 =
eval vs P * vs v + eval vs Q1 * vs w + eval vs Q2 rewrite (plus_comm (eval vs Q1 * vs w)).
C: Type
V: Type0
Aplus: canonical_names.Plus C
Amult: canonical_names.Mult C
Azero: canonical_names.Zero C
Aone: canonical_names.One C
Anegate: AlmostNegate C
H: AlmostRing C
H0: DecidablePaths C
Vlt: Relation V
H1: Trichotomy Vlt
R: Type
Aplus0: canonical_names.Plus R
Amult0: canonical_names.Mult R
Azero0: canonical_names.Zero R
Aone0: canonical_names.One R
Anegate0: AlmostNegate R
H2: AlmostRing R
phi: Vars C
AlmostRingPreserving0: AlmostRingPreserving phi
vs: Vars V
P: Pol
addP: Pol -> Pol
Eadd: forall Q : Pol,
eval vs (addP Q) = eval vs P + eval vs Q
v: V
Q1: Pol
w: V
Q2: Pol
IH1: eval vs (add_aux addP P v Q1) =
eval vs P * vs v + eval vs Q1
IH2: eval vs (add_aux addP P v Q2) =
eval vs P * vs v + eval vs Q2
eval vs P * vs v + eval vs Q1 * vs w + eval vs Q2 =
eval vs P * vs v + eval vs Q1 * vs w + eval vs Q2
    reflexivity.
  +
C: Type
V: Type0
Aplus: canonical_names.Plus C
Amult: canonical_names.Mult C
Azero: canonical_names.Zero C
Aone: canonical_names.One C
Anegate: AlmostNegate C
H: AlmostRing C
H0: DecidablePaths C
Vlt: Relation V
H1: Trichotomy Vlt
R: Type
Aplus0: canonical_names.Plus R
Amult0: canonical_names.Mult R
Azero0: canonical_names.Zero R
Aone0: canonical_names.One R
Anegate0: AlmostNegate R
H2: AlmostRing R
phi: Vars C
AlmostRingPreserving0: AlmostRingPreserving phi
vs: Vars V
P: Pol
addP: Pol -> Pol
Eadd: forall Q : Pol,
eval vs (addP Q) = eval vs P + eval vs Q
v: V
Q1, Q2: Pol
IH1: eval vs (add_aux addP P v Q1) =
eval vs P * vs v + eval vs Q1
IH2: eval vs (add_aux addP P v Q2) =
eval vs P * vs v + eval vs Q2
eval vs (PXguard (addP Q1) v Q2) =
eval vs P * vs v + (eval vs Q1 * vs v + eval vs Q2) rewrite eval_PXguard.
C: Type
V: Type0
Aplus: canonical_names.Plus C
Amult: canonical_names.Mult C
Azero: canonical_names.Zero C
Aone: canonical_names.One C
Anegate: AlmostNegate C
H: AlmostRing C
H0: DecidablePaths C
Vlt: Relation V
H1: Trichotomy Vlt
R: Type
Aplus0: canonical_names.Plus R
Amult0: canonical_names.Mult R
Azero0: canonical_names.Zero R
Aone0: canonical_names.One R
Anegate0: AlmostNegate R
H2: AlmostRing R
phi: Vars C
AlmostRingPreserving0: AlmostRingPreserving phi
vs: Vars V
P: Pol
addP: Pol -> Pol
Eadd: forall Q : Pol,
eval vs (addP Q) = eval vs P + eval vs Q
v: V
Q1, Q2: Pol
IH1: eval vs (add_aux addP P v Q1) =
eval vs P * vs v + eval vs Q1
IH2: eval vs (add_aux addP P v Q2) =
eval vs P * vs v + eval vs Q2
eval vs (addP Q1) * vs v + eval vs Q2 =
eval vs P * vs v + (eval vs Q1 * vs v + eval vs Q2) rewrite Eadd.
C: Type
V: Type0
Aplus: canonical_names.Plus C
Amult: canonical_names.Mult C
Azero: canonical_names.Zero C
Aone: canonical_names.One C
Anegate: AlmostNegate C
H: AlmostRing C
H0: DecidablePaths C
Vlt: Relation V
H1: Trichotomy Vlt
R: Type
Aplus0: canonical_names.Plus R
Amult0: canonical_names.Mult R
Azero0: canonical_names.Zero R
Aone0: canonical_names.One R
Anegate0: AlmostNegate R
H2: AlmostRing R
phi: Vars C
AlmostRingPreserving0: AlmostRingPreserving phi
vs: Vars V
P: Pol
addP: Pol -> Pol
Eadd: forall Q : Pol,
eval vs (addP Q) = eval vs P + eval vs Q
v: V
Q1, Q2: Pol
IH1: eval vs (add_aux addP P v Q1) =
eval vs P * vs v + eval vs Q1
IH2: eval vs (add_aux addP P v Q2) =
eval vs P * vs v + eval vs Q2
(eval vs P + eval vs Q1) * vs v + eval vs Q2 =
eval vs P * vs v + (eval vs Q1 * vs v + eval vs Q2)
    rewrite plus_mult_distr_r.
C: Type
V: Type0
Aplus: canonical_names.Plus C
Amult: canonical_names.Mult C
Azero: canonical_names.Zero C
Aone: canonical_names.One C
Anegate: AlmostNegate C
H: AlmostRing C
H0: DecidablePaths C
Vlt: Relation V
H1: Trichotomy Vlt
R: Type
Aplus0: canonical_names.Plus R
Amult0: canonical_names.Mult R
Azero0: canonical_names.Zero R
Aone0: canonical_names.One R
Anegate0: AlmostNegate R
H2: AlmostRing R
phi: Vars C
AlmostRingPreserving0: AlmostRingPreserving phi
vs: Vars V
P: Pol
addP: Pol -> Pol
Eadd: forall Q : Pol,
eval vs (addP Q) = eval vs P + eval vs Q
v: V
Q1, Q2: Pol
IH1: eval vs (add_aux addP P v Q1) =
eval vs P * vs v + eval vs Q1
IH2: eval vs (add_aux addP P v Q2) =
eval vs P * vs v + eval vs Q2
eval vs P * vs v + eval vs Q1 * vs v + eval vs Q2 =
eval vs P * vs v + (eval vs Q1 * vs v + eval vs Q2)
    symmetry;apply plus_assoc.
  +
C: Type
V: Type0
Aplus: canonical_names.Plus C
Amult: canonical_names.Mult C
Azero: canonical_names.Zero C
Aone: canonical_names.One C
Anegate: AlmostNegate C
H: AlmostRing C
H0: DecidablePaths C
Vlt: Relation V
H1: Trichotomy Vlt
R: Type
Aplus0: canonical_names.Plus R
Amult0: canonical_names.Mult R
Azero0: canonical_names.Zero R
Aone0: canonical_names.One R
Anegate0: AlmostNegate R
H2: AlmostRing R
phi: Vars C
AlmostRingPreserving0: AlmostRingPreserving phi
vs: Vars V
P: Pol
addP: Pol -> Pol
Eadd: forall Q : Pol,
eval vs (addP Q) = eval vs P + eval vs Q
v: V
Q1: Pol
w: V
Q2: Pol
IH1: eval vs (add_aux addP P v Q1) =
eval vs P * vs v + eval vs Q1
IH2: eval vs (add_aux addP P v Q2) =
eval vs P * vs v + eval vs Q2
eval vs (PX P v (PX Q1 w Q2)) =
eval vs P * vs v + (eval vs Q1 * vs w + eval vs Q2) simpl.
C: Type
V: Type0
Aplus: canonical_names.Plus C
Amult: canonical_names.Mult C
Azero: canonical_names.Zero C
Aone: canonical_names.One C
Anegate: AlmostNegate C
H: AlmostRing C
H0: DecidablePaths C
Vlt: Relation V
H1: Trichotomy Vlt
R: Type
Aplus0: canonical_names.Plus R
Amult0: canonical_names.Mult R
Azero0: canonical_names.Zero R
Aone0: canonical_names.One R
Anegate0: AlmostNegate R
H2: AlmostRing R
phi: Vars C
AlmostRingPreserving0: AlmostRingPreserving phi
vs: Vars V
P: Pol
addP: Pol -> Pol
Eadd: forall Q : Pol,
eval vs (addP Q) = eval vs P + eval vs Q
v: V
Q1: Pol
w: V
Q2: Pol
IH1: eval vs (add_aux addP P v Q1) =
eval vs P * vs v + eval vs Q1
IH2: eval vs (add_aux addP P v Q2) =
eval vs P * vs v + eval vs Q2
eval vs P * vs v + (eval vs Q1 * vs w + eval vs Q2) =
eval vs P * vs v + (eval vs Q1 * vs w + eval vs Q2) reflexivity.
Qed.

Lemma eval_add' vs : forall P Q, eval vs (add P Q) = eval vs P + eval vs Q.
C: Type
V: Type0
Aplus: canonical_names.Plus C
Amult: canonical_names.Mult C
Azero: canonical_names.Zero C
Aone: canonical_names.One C
Anegate: AlmostNegate C
H: AlmostRing C
H0: DecidablePaths C
Vlt: Relation V
H1: Trichotomy Vlt
R: Type
Aplus0: canonical_names.Plus R
Amult0: canonical_names.Mult R
Azero0: canonical_names.Zero R
Aone0: canonical_names.One R
Anegate0: AlmostNegate R
H2: AlmostRing R
phi: Vars C
AlmostRingPreserving0: AlmostRingPreserving phi
vs: Vars V
forall P Q : Pol,
eval vs (add P Q) = eval vs P + eval vs Q
Proof.
C: Type
V: Type0
Aplus: canonical_names.Plus C
Amult: canonical_names.Mult C
Azero: canonical_names.Zero C
Aone: canonical_names.One C
Anegate: AlmostNegate C
H: AlmostRing C
H0: DecidablePaths C
Vlt: Relation V
H1: Trichotomy Vlt
R: Type
Aplus0: canonical_names.Plus R
Amult0: canonical_names.Mult R
Azero0: canonical_names.Zero R
Aone0: canonical_names.One R
Anegate0: AlmostNegate R
H2: AlmostRing R
phi: Vars C
AlmostRingPreserving0: AlmostRingPreserving phi
vs: Vars V
forall P Q : Pol,
eval vs (add P Q) = eval vs P + eval vs Q
induction P as [c|P1 IH1 v P2 IH2];intros Q.
C: Type
V: Type0
Aplus: canonical_names.Plus C
Amult: canonical_names.Mult C
Azero: canonical_names.Zero C
Aone: canonical_names.One C
Anegate: AlmostNegate C
H: AlmostRing C
H0: DecidablePaths C
Vlt: Relation V
H1: Trichotomy Vlt
R: Type
Aplus0: canonical_names.Plus R
Amult0: canonical_names.Mult R
Azero0: canonical_names.Zero R
Aone0: canonical_names.One R
Anegate0: AlmostNegate R
H2: AlmostRing R
phi: Vars C
AlmostRingPreserving0: AlmostRingPreserving phi
vs: Vars V
c: C
Q: Pol
eval vs (add (Pconst c) Q) =
eval vs (Pconst c) + eval vs Q
C: Type
V: Type0
Aplus: canonical_names.Plus C
Amult: canonical_names.Mult C
Azero: canonical_names.Zero C
Aone: canonical_names.One C
Anegate: AlmostNegate C
H: AlmostRing C
H0: DecidablePaths C
Vlt: Relation V
H1: Trichotomy Vlt
R: Type
Aplus0: canonical_names.Plus R
Amult0: canonical_names.Mult R
Azero0: canonical_names.Zero R
Aone0: canonical_names.One R
Anegate0: AlmostNegate R
H2: AlmostRing R
phi: Vars C
AlmostRingPreserving0: AlmostRingPreserving phi
vs: Vars V
P1: Pol
v: V
P2: Pol
IH1: forall Q : Pol,
eval vs (add P1 Q) = eval vs P1 + eval vs Q
IH2: forall Q : Pol,
eval vs (add P2 Q) = eval vs P2 + eval vs Q
Q: Pol
eval vs (add (PX P1 v P2) Q) =
eval vs (PX P1 v P2) + eval vs Q
-
C: Type
V: Type0
Aplus: canonical_names.Plus C
Amult: canonical_names.Mult C
Azero: canonical_names.Zero C
Aone: canonical_names.One C
Anegate: AlmostNegate C
H: AlmostRing C
H0: DecidablePaths C
Vlt: Relation V
H1: Trichotomy Vlt
R: Type
Aplus0: canonical_names.Plus R
Amult0: canonical_names.Mult R
Azero0: canonical_names.Zero R
Aone0: canonical_names.One R
Anegate0: AlmostNegate R
H2: AlmostRing R
phi: Vars C
AlmostRingPreserving0: AlmostRingPreserving phi
vs: Vars V
c: C
Q: Pol
eval vs (add (Pconst c) Q) =
eval vs (Pconst c) + eval vs Q simpl.
C: Type
V: Type0
Aplus: canonical_names.Plus C
Amult: canonical_names.Mult C
Azero: canonical_names.Zero C
Aone: canonical_names.One C
Anegate: AlmostNegate C
H: AlmostRing C
H0: DecidablePaths C
Vlt: Relation V
H1: Trichotomy Vlt
R: Type
Aplus0: canonical_names.Plus R
Amult0: canonical_names.Mult R
Azero0: canonical_names.Zero R
Aone0: canonical_names.One R
Anegate0: AlmostNegate R
H2: AlmostRing R
phi: Vars C
AlmostRingPreserving0: AlmostRingPreserving phi
vs: Vars V
c: C
Q: Pol
eval vs (addC c Q) = phi c + eval vs Q apply eval_addC.
-
C: Type
V: Type0
Aplus: canonical_names.Plus C
Amult: canonical_names.Mult C
Azero: canonical_names.Zero C
Aone: canonical_names.One C
Anegate: AlmostNegate C
H: AlmostRing C
H0: DecidablePaths C
Vlt: Relation V
H1: Trichotomy Vlt
R: Type
Aplus0: canonical_names.Plus R
Amult0: canonical_names.Mult R
Azero0: canonical_names.Zero R
Aone0: canonical_names.One R
Anegate0: AlmostNegate R
H2: AlmostRing R
phi: Vars C
AlmostRingPreserving0: AlmostRingPreserving phi
vs: Vars V
P1: Pol
v: V
P2: Pol
IH1: forall Q : Pol,
eval vs (add P1 Q) = eval vs P1 + eval vs Q
IH2: forall Q : Pol,
eval vs (add P2 Q) = eval vs P2 + eval vs Q
Q: Pol
eval vs (add (PX P1 v P2) Q) =
eval vs (PX P1 v P2) + eval vs Q simpl.
C: Type
V: Type0
Aplus: canonical_names.Plus C
Amult: canonical_names.Mult C
Azero: canonical_names.Zero C
Aone: canonical_names.One C
Anegate: AlmostNegate C
H: AlmostRing C
H0: DecidablePaths C
Vlt: Relation V
H1: Trichotomy Vlt
R: Type
Aplus0: canonical_names.Plus R
Amult0: canonical_names.Mult R
Azero0: canonical_names.Zero R
Aone0: canonical_names.One R
Anegate0: AlmostNegate R
H2: AlmostRing R
phi: Vars C
AlmostRingPreserving0: AlmostRingPreserving phi
vs: Vars V
P1: Pol
v: V
P2: Pol
IH1: forall Q : Pol,
eval vs (add P1 Q) = eval vs P1 + eval vs Q
IH2: forall Q : Pol,
eval vs (add P2 Q) = eval vs P2 + eval vs Q
Q: Pol
eval vs (add_aux (add P1) P1 v (add P2 Q)) =
eval vs P1 * vs v + eval vs P2 + eval vs Q rewrite eval_add_aux;auto.
C: Type
V: Type0
Aplus: canonical_names.Plus C
Amult: canonical_names.Mult C
Azero: canonical_names.Zero C
Aone: canonical_names.One C
Anegate: AlmostNegate C
H: AlmostRing C
H0: DecidablePaths C
Vlt: Relation V
H1: Trichotomy Vlt
R: Type
Aplus0: canonical_names.Plus R
Amult0: canonical_names.Mult R
Azero0: canonical_names.Zero R
Aone0: canonical_names.One R
Anegate0: AlmostNegate R
H2: AlmostRing R
phi: Vars C
AlmostRingPreserving0: AlmostRingPreserving phi
vs: Vars V
P1: Pol
v: V
P2: Pol
IH1: forall Q : Pol,
eval vs (add P1 Q) = eval vs P1 + eval vs Q
IH2: forall Q : Pol,
eval vs (add P2 Q) = eval vs P2 + eval vs Q
Q: Pol
eval vs P1 * vs v + eval vs (add P2 Q) =
eval vs P1 * vs v + eval vs P2 + eval vs Q
  rewrite IH2.
C: Type
V: Type0
Aplus: canonical_names.Plus C
Amult: canonical_names.Mult C
Azero: canonical_names.Zero C
Aone: canonical_names.One C
Anegate: AlmostNegate C
H: AlmostRing C
H0: DecidablePaths C
Vlt: Relation V
H1: Trichotomy Vlt
R: Type
Aplus0: canonical_names.Plus R
Amult0: canonical_names.Mult R
Azero0: canonical_names.Zero R
Aone0: canonical_names.One R
Anegate0: AlmostNegate R
H2: AlmostRing R
phi: Vars C
AlmostRingPreserving0: AlmostRingPreserving phi
vs: Vars V
P1: Pol
v: V
P2: Pol
IH1: forall Q : Pol,
eval vs (add P1 Q) = eval vs P1 + eval vs Q
IH2: forall Q : Pol,
eval vs (add P2 Q) = eval vs P2 + eval vs Q
Q: Pol
eval vs P1 * vs v + (eval vs P2 + eval vs Q) =
eval vs P1 * vs v + eval vs P2 + eval vs Q apply plus_assoc.
Qed.

Definition eval_add@{} := ltac:(first [exact eval_add'@{Ularge}|
                                       exact eval_add'@{}]).

Fixpoint mulX v P :=
  match P with
  | Pconst c => addX c v 0
  | PX P1 w P2 =>
    match v ?= w with
    | LT =>
      PX (mulX v P1) w (mulX v P2)
    | _ => PX P v 0
    end
  end.

Lemma eval_mulX@{} vs : forall (v:V) (P:Pol), eval vs (mulX v P) = eval vs P * vs v.
C: Type
V: Type0
Aplus: canonical_names.Plus C
Amult: canonical_names.Mult C
Azero: canonical_names.Zero C
Aone: canonical_names.One C
Anegate: AlmostNegate C
H: AlmostRing C
H0: DecidablePaths C
Vlt: Relation V
H1: Trichotomy Vlt
R: Type
Aplus0: canonical_names.Plus R
Amult0: canonical_names.Mult R
Azero0: canonical_names.Zero R
Aone0: canonical_names.One R
Anegate0: AlmostNegate R
H2: AlmostRing R
phi: Vars C
AlmostRingPreserving0: AlmostRingPreserving phi
vs: Vars V
forall (v : V) (P : Pol),
eval vs (mulX v P) = eval vs P * vs v
Proof.
C: Type
V: Type0
Aplus: canonical_names.Plus C
Amult: canonical_names.Mult C
Azero: canonical_names.Zero C
Aone: canonical_names.One C
Anegate: AlmostNegate C
H: AlmostRing C
H0: DecidablePaths C
Vlt: Relation V
H1: Trichotomy Vlt
R: Type
Aplus0: canonical_names.Plus R
Amult0: canonical_names.Mult R
Azero0: canonical_names.Zero R
Aone0: canonical_names.One R
Anegate0: AlmostNegate R
H2: AlmostRing R
phi: Vars C
AlmostRingPreserving0: AlmostRingPreserving phi
vs: Vars V
forall (v : V) (P : Pol),
eval vs (mulX v P) = eval vs P * vs v
induction P as [c|P1 IH1 w P2 IH2].
C: Type
V: Type0
Aplus: canonical_names.Plus C
Amult: canonical_names.Mult C
Azero: canonical_names.Zero C
Aone: canonical_names.One C
Anegate: AlmostNegate C
H: AlmostRing C
H0: DecidablePaths C
Vlt: Relation V
H1: Trichotomy Vlt
R: Type
Aplus0: canonical_names.Plus R
Amult0: canonical_names.Mult R
Azero0: canonical_names.Zero R
Aone0: canonical_names.One R
Anegate0: AlmostNegate R
H2: AlmostRing R
phi: Vars C
AlmostRingPreserving0: AlmostRingPreserving phi
vs: Vars V
v: V
c: C
eval vs (mulX v (Pconst c)) =
eval vs (Pconst c) * vs v
C: Type
V: Type0
Aplus: canonical_names.Plus C
Amult: canonical_names.Mult C
Azero: canonical_names.Zero C
Aone: canonical_names.One C
Anegate: AlmostNegate C
H: AlmostRing C
H0: DecidablePaths C
Vlt: Relation V
H1: Trichotomy Vlt
R: Type
Aplus0: canonical_names.Plus R
Amult0: canonical_names.Mult R
Azero0: canonical_names.Zero R
Aone0: canonical_names.One R
Anegate0: AlmostNegate R
H2: AlmostRing R
phi: Vars C
AlmostRingPreserving0: AlmostRingPreserving phi
vs: Vars V
v: V
P1: Pol
w: V
P2: Pol
IH1: eval vs (mulX v P1) = eval vs P1 * vs v
IH2: eval vs (mulX v P2) = eval vs P2 * vs v
eval vs (mulX v (PX P1 w P2)) =
eval vs (PX P1 w P2) * vs v
-
C: Type
V: Type0
Aplus: canonical_names.Plus C
Amult: canonical_names.Mult C
Azero: canonical_names.Zero C
Aone: canonical_names.One C
Anegate: AlmostNegate C
H: AlmostRing C
H0: DecidablePaths C
Vlt: Relation V
H1: Trichotomy Vlt
R: Type
Aplus0: canonical_names.Plus R
Amult0: canonical_names.Mult R
Azero0: canonical_names.Zero R
Aone0: canonical_names.One R
Anegate0: AlmostNegate R
H2: AlmostRing R
phi: Vars C
AlmostRingPreserving0: AlmostRingPreserving phi
vs: Vars V
v: V
c: C
eval vs (mulX v (Pconst c)) =
eval vs (Pconst c) * vs v simpl.
C: Type
V: Type0
Aplus: canonical_names.Plus C
Amult: canonical_names.Mult C
Azero: canonical_names.Zero C
Aone: canonical_names.One C
Anegate: AlmostNegate C
H: AlmostRing C
H0: DecidablePaths C
Vlt: Relation V
H1: Trichotomy Vlt
R: Type
Aplus0: canonical_names.Plus R
Amult0: canonical_names.Mult R
Azero0: canonical_names.Zero R
Aone0: canonical_names.One R
Anegate0: AlmostNegate R
H2: AlmostRing R
phi: Vars C
AlmostRingPreserving0: AlmostRingPreserving phi
vs: Vars V
v: V
c: C
eval vs (addX c v 0) = phi c * vs v rewrite eval_addX.
C: Type
V: Type0
Aplus: canonical_names.Plus C
Amult: canonical_names.Mult C
Azero: canonical_names.Zero C
Aone: canonical_names.One C
Anegate: AlmostNegate C
H: AlmostRing C
H0: DecidablePaths C
Vlt: Relation V
H1: Trichotomy Vlt
R: Type
Aplus0: canonical_names.Plus R
Amult0: canonical_names.Mult R
Azero0: canonical_names.Zero R
Aone0: canonical_names.One R
Anegate0: AlmostNegate R
H2: AlmostRing R
phi: Vars C
AlmostRingPreserving0: AlmostRingPreserving phi
vs: Vars V
v: V
c: C
phi c * vs v + eval vs 0 = phi c * vs v
  simpl.
C: Type
V: Type0
Aplus: canonical_names.Plus C
Amult: canonical_names.Mult C
Azero: canonical_names.Zero C
Aone: canonical_names.One C
Anegate: AlmostNegate C
H: AlmostRing C
H0: DecidablePaths C
Vlt: Relation V
H1: Trichotomy Vlt
R: Type
Aplus0: canonical_names.Plus R
Amult0: canonical_names.Mult R
Azero0: canonical_names.Zero R
Aone0: canonical_names.One R
Anegate0: AlmostNegate R
H2: AlmostRing R
phi: Vars C
AlmostRingPreserving0: AlmostRingPreserving phi
vs: Vars V
v: V
c: C
phi c * vs v + phi 0 = phi c * vs v rewrite (preserves_0 (f:=phi)),plus_0_r.
C: Type
V: Type0
Aplus: canonical_names.Plus C
Amult: canonical_names.Mult C
Azero: canonical_names.Zero C
Aone: canonical_names.One C
Anegate: AlmostNegate C
H: AlmostRing C
H0: DecidablePaths C
Vlt: Relation V
H1: Trichotomy Vlt
R: Type
Aplus0: canonical_names.Plus R
Amult0: canonical_names.Mult R
Azero0: canonical_names.Zero R
Aone0: canonical_names.One R
Anegate0: AlmostNegate R
H2: AlmostRing R
phi: Vars C
AlmostRingPreserving0: AlmostRingPreserving phi
vs: Vars V
v: V
c: C
phi c * vs v = phi c * vs v
  split.
-
C: Type
V: Type0
Aplus: canonical_names.Plus C
Amult: canonical_names.Mult C
Azero: canonical_names.Zero C
Aone: canonical_names.One C
Anegate: AlmostNegate C
H: AlmostRing C
H0: DecidablePaths C
Vlt: Relation V
H1: Trichotomy Vlt
R: Type
Aplus0: canonical_names.Plus R
Amult0: canonical_names.Mult R
Azero0: canonical_names.Zero R
Aone0: canonical_names.One R
Anegate0: AlmostNegate R
H2: AlmostRing R
phi: Vars C
AlmostRingPreserving0: AlmostRingPreserving phi
vs: Vars V
v: V
P1: Pol
w: V
P2: Pol
IH1: eval vs (mulX v P1) = eval vs P1 * vs v
IH2: eval vs (mulX v P2) = eval vs P2 * vs v
eval vs (mulX v (PX P1 w P2)) =
eval vs (PX P1 w P2) * vs v simpl.
C: Type
V: Type0
Aplus: canonical_names.Plus C
Amult: canonical_names.Mult C
Azero: canonical_names.Zero C
Aone: canonical_names.One C
Anegate: AlmostNegate C
H: AlmostRing C
H0: DecidablePaths C
Vlt: Relation V
H1: Trichotomy Vlt
R: Type
Aplus0: canonical_names.Plus R
Amult0: canonical_names.Mult R
Azero0: canonical_names.Zero R
Aone0: canonical_names.One R
Anegate0: AlmostNegate R
H2: AlmostRing R
phi: Vars C
AlmostRingPreserving0: AlmostRingPreserving phi
vs: Vars V
v: V
P1: Pol
w: V
P2: Pol
IH1: eval vs (mulX v P1) = eval vs P1 * vs v
IH2: eval vs (mulX v P2) = eval vs P2 * vs v
eval vs
  match v ?= w with
  | LT => PX (mulX v P1) w (mulX v P2)
  | _ => PX (PX P1 w P2) v 0
  end = (eval vs P1 * vs w + eval vs P2) * vs v
  pose proof (tricho_compare_eq v w) as E.
C: Type
V: Type0
Aplus: canonical_names.Plus C
Amult: canonical_names.Mult C
Azero: canonical_names.Zero C
Aone: canonical_names.One C
Anegate: AlmostNegate C
H: AlmostRing C
H0: DecidablePaths C
Vlt: Relation V
H1: Trichotomy Vlt
R: Type
Aplus0: canonical_names.Plus R
Amult0: canonical_names.Mult R
Azero0: canonical_names.Zero R
Aone0: canonical_names.One R
Anegate0: AlmostNegate R
H2: AlmostRing R
phi: Vars C
AlmostRingPreserving0: AlmostRingPreserving phi
vs: Vars V
v: V
P1: Pol
w: V
P2: Pol
IH1: eval vs (mulX v P1) = eval vs P1 * vs v
IH2: eval vs (mulX v P2) = eval vs P2 * vs v
E: (v ?= w) = EQ -> v = w
eval vs
  match v ?= w with
  | LT => PX (mulX v P1) w (mulX v P2)
  | _ => PX (PX P1 w P2) v 0
  end = (eval vs P1 * vs w + eval vs P2) * vs v
  destruct (v ?= w);[clear E|rewrite <-E by split;clear E w|clear E].
C: Type
V: Type0
Aplus: canonical_names.Plus C
Amult: canonical_names.Mult C
Azero: canonical_names.Zero C
Aone: canonical_names.One C
Anegate: AlmostNegate C
H: AlmostRing C
H0: DecidablePaths C
Vlt: Relation V
H1: Trichotomy Vlt
R: Type
Aplus0: canonical_names.Plus R
Amult0: canonical_names.Mult R
Azero0: canonical_names.Zero R
Aone0: canonical_names.One R
Anegate0: AlmostNegate R
H2: AlmostRing R
phi: Vars C
AlmostRingPreserving0: AlmostRingPreserving phi
vs: Vars V
v: V
P1: Pol
w: V
P2: Pol
IH1: eval vs (mulX v P1) = eval vs P1 * vs v
IH2: eval vs (mulX v P2) = eval vs P2 * vs v
eval vs (PX (mulX v P1) w (mulX v P2)) =
(eval vs P1 * vs w + eval vs P2) * vs v
C: Type
V: Type0
Aplus: canonical_names.Plus C
Amult: canonical_names.Mult C
Azero: canonical_names.Zero C
Aone: canonical_names.One C
Anegate: AlmostNegate C
H: AlmostRing C
H0: DecidablePaths C
Vlt: Relation V
H1: Trichotomy Vlt
R: Type
Aplus0: canonical_names.Plus R
Amult0: canonical_names.Mult R
Azero0: canonical_names.Zero R
Aone0: canonical_names.One R
Anegate0: AlmostNegate R
H2: AlmostRing R
phi: Vars C
AlmostRingPreserving0: AlmostRingPreserving phi
vs: Vars V
v: V
P1, P2: Pol
IH1: eval vs (mulX v P1) = eval vs P1 * vs v
IH2: eval vs (mulX v P2) = eval vs P2 * vs v
eval vs (PX (PX P1 v P2) v 0) =
(eval vs P1 * vs v + eval vs P2) * vs v
C: Type
V: Type0
Aplus: canonical_names.Plus C
Amult: canonical_names.Mult C
Azero: canonical_names.Zero C
Aone: canonical_names.One C
Anegate: AlmostNegate C
H: AlmostRing C
H0: DecidablePaths C
Vlt: Relation V
H1: Trichotomy Vlt
R: Type
Aplus0: canonical_names.Plus R
Amult0: canonical_names.Mult R
Azero0: canonical_names.Zero R
Aone0: canonical_names.One R
Anegate0: AlmostNegate R
H2: AlmostRing R
phi: Vars C
AlmostRingPreserving0: AlmostRingPreserving phi
vs: Vars V
v: V
P1: Pol
w: V
P2: Pol
IH1: eval vs (mulX v P1) = eval vs P1 * vs v
IH2: eval vs (mulX v P2) = eval vs P2 * vs v
eval vs (PX (PX P1 w P2) v 0) =
(eval vs P1 * vs w + eval vs P2) * vs v
  +
C: Type
V: Type0
Aplus: canonical_names.Plus C
Amult: canonical_names.Mult C
Azero: canonical_names.Zero C
Aone: canonical_names.One C
Anegate: AlmostNegate C
H: AlmostRing C
H0: DecidablePaths C
Vlt: Relation V
H1: Trichotomy Vlt
R: Type
Aplus0: canonical_names.Plus R
Amult0: canonical_names.Mult R
Azero0: canonical_names.Zero R
Aone0: canonical_names.One R
Anegate0: AlmostNegate R
H2: AlmostRing R
phi: Vars C
AlmostRingPreserving0: AlmostRingPreserving phi
vs: Vars V
v: V
P1: Pol
w: V
P2: Pol
IH1: eval vs (mulX v P1) = eval vs P1 * vs v
IH2: eval vs (mulX v P2) = eval vs P2 * vs v
eval vs (PX (mulX v P1) w (mulX v P2)) =
(eval vs P1 * vs w + eval vs P2) * vs v simpl.
C: Type
V: Type0
Aplus: canonical_names.Plus C
Amult: canonical_names.Mult C
Azero: canonical_names.Zero C
Aone: canonical_names.One C
Anegate: AlmostNegate C
H: AlmostRing C
H0: DecidablePaths C
Vlt: Relation V
H1: Trichotomy Vlt
R: Type
Aplus0: canonical_names.Plus R
Amult0: canonical_names.Mult R
Azero0: canonical_names.Zero R
Aone0: canonical_names.One R
Anegate0: AlmostNegate R
H2: AlmostRing R
phi: Vars C
AlmostRingPreserving0: AlmostRingPreserving phi
vs: Vars V
v: V
P1: Pol
w: V
P2: Pol
IH1: eval vs (mulX v P1) = eval vs P1 * vs v
IH2: eval vs (mulX v P2) = eval vs P2 * vs v
eval vs (mulX v P1) * vs w + eval vs (mulX v P2) =
(eval vs P1 * vs w + eval vs P2) * vs v
    rewrite plus_mult_distr_r,IH1,IH2.
C: Type
V: Type0
Aplus: canonical_names.Plus C
Amult: canonical_names.Mult C
Azero: canonical_names.Zero C
Aone: canonical_names.One C
Anegate: AlmostNegate C
H: AlmostRing C
H0: DecidablePaths C
Vlt: Relation V
H1: Trichotomy Vlt
R: Type
Aplus0: canonical_names.Plus R
Amult0: canonical_names.Mult R
Azero0: canonical_names.Zero R
Aone0: canonical_names.One R
Anegate0: AlmostNegate R
H2: AlmostRing R
phi: Vars C
AlmostRingPreserving0: AlmostRingPreserving phi
vs: Vars V
v: V
P1: Pol
w: V
P2: Pol
IH1: eval vs (mulX v P1) = eval vs P1 * vs v
IH2: eval vs (mulX v P2) = eval vs P2 * vs v
eval vs P1 * vs v * vs w + eval vs P2 * vs v =
eval vs P1 * vs w * vs v + eval vs P2 * vs v
    apply ap011;trivial.
C: Type
V: Type0
Aplus: canonical_names.Plus C
Amult: canonical_names.Mult C
Azero: canonical_names.Zero C
Aone: canonical_names.One C
Anegate: AlmostNegate C
H: AlmostRing C
H0: DecidablePaths C
Vlt: Relation V
H1: Trichotomy Vlt
R: Type
Aplus0: canonical_names.Plus R
Amult0: canonical_names.Mult R
Azero0: canonical_names.Zero R
Aone0: canonical_names.One R
Anegate0: AlmostNegate R
H2: AlmostRing R
phi: Vars C
AlmostRingPreserving0: AlmostRingPreserving phi
vs: Vars V
v: V
P1: Pol
w: V
P2: Pol
IH1: eval vs (mulX v P1) = eval vs P1 * vs v
IH2: eval vs (mulX v P2) = eval vs P2 * vs v
eval vs P1 * vs v * vs w = eval vs P1 * vs w * vs v
    rewrite <-2!mult_assoc;apply ap,mult_comm.
  +
C: Type
V: Type0
Aplus: canonical_names.Plus C
Amult: canonical_names.Mult C
Azero: canonical_names.Zero C
Aone: canonical_names.One C
Anegate: AlmostNegate C
H: AlmostRing C
H0: DecidablePaths C
Vlt: Relation V
H1: Trichotomy Vlt
R: Type
Aplus0: canonical_names.Plus R
Amult0: canonical_names.Mult R
Azero0: canonical_names.Zero R
Aone0: canonical_names.One R
Anegate0: AlmostNegate R
H2: AlmostRing R
phi: Vars C
AlmostRingPreserving0: AlmostRingPreserving phi
vs: Vars V
v: V
P1, P2: Pol
IH1: eval vs (mulX v P1) = eval vs P1 * vs v
IH2: eval vs (mulX v P2) = eval vs P2 * vs v
eval vs (PX (PX P1 v P2) v 0) =
(eval vs P1 * vs v + eval vs P2) * vs v simpl.
C: Type
V: Type0
Aplus: canonical_names.Plus C
Amult: canonical_names.Mult C
Azero: canonical_names.Zero C
Aone: canonical_names.One C
Anegate: AlmostNegate C
H: AlmostRing C
H0: DecidablePaths C
Vlt: Relation V
H1: Trichotomy Vlt
R: Type
Aplus0: canonical_names.Plus R
Amult0: canonical_names.Mult R
Azero0: canonical_names.Zero R
Aone0: canonical_names.One R
Anegate0: AlmostNegate R
H2: AlmostRing R
phi: Vars C
AlmostRingPreserving0: AlmostRingPreserving phi
vs: Vars V
v: V
P1, P2: Pol
IH1: eval vs (mulX v P1) = eval vs P1 * vs v
IH2: eval vs (mulX v P2) = eval vs P2 * vs v
(eval vs P1 * vs v + eval vs P2) * vs v + phi 0 =
(eval vs P1 * vs v + eval vs P2) * vs v rewrite (preserves_0 (f:=phi)),plus_0_r.
C: Type
V: Type0
Aplus: canonical_names.Plus C
Amult: canonical_names.Mult C
Azero: canonical_names.Zero C
Aone: canonical_names.One C
Anegate: AlmostNegate C
H: AlmostRing C
H0: DecidablePaths C
Vlt: Relation V
H1: Trichotomy Vlt
R: Type
Aplus0: canonical_names.Plus R
Amult0: canonical_names.Mult R
Azero0: canonical_names.Zero R
Aone0: canonical_names.One R
Anegate0: AlmostNegate R
H2: AlmostRing R
phi: Vars C
AlmostRingPreserving0: AlmostRingPreserving phi
vs: Vars V
v: V
P1, P2: Pol
IH1: eval vs (mulX v P1) = eval vs P1 * vs v
IH2: eval vs (mulX v P2) = eval vs P2 * vs v
(eval vs P1 * vs v + eval vs P2) * vs v =
(eval vs P1 * vs v + eval vs P2) * vs v
    reflexivity.
  +
C: Type
V: Type0
Aplus: canonical_names.Plus C
Amult: canonical_names.Mult C
Azero: canonical_names.Zero C
Aone: canonical_names.One C
Anegate: AlmostNegate C
H: AlmostRing C
H0: DecidablePaths C
Vlt: Relation V
H1: Trichotomy Vlt
R: Type
Aplus0: canonical_names.Plus R
Amult0: canonical_names.Mult R
Azero0: canonical_names.Zero R
Aone0: canonical_names.One R
Anegate0: AlmostNegate R
H2: AlmostRing R
phi: Vars C
AlmostRingPreserving0: AlmostRingPreserving phi
vs: Vars V
v: V
P1: Pol
w: V
P2: Pol
IH1: eval vs (mulX v P1) = eval vs P1 * vs v
IH2: eval vs (mulX v P2) = eval vs P2 * vs v
eval vs (PX (PX P1 w P2) v 0) =
(eval vs P1 * vs w + eval vs P2) * vs v simpl.
C: Type
V: Type0
Aplus: canonical_names.Plus C
Amult: canonical_names.Mult C
Azero: canonical_names.Zero C
Aone: canonical_names.One C
Anegate: AlmostNegate C
H: AlmostRing C
H0: DecidablePaths C
Vlt: Relation V
H1: Trichotomy Vlt
R: Type
Aplus0: canonical_names.Plus R
Amult0: canonical_names.Mult R
Azero0: canonical_names.Zero R
Aone0: canonical_names.One R
Anegate0: AlmostNegate R
H2: AlmostRing R
phi: Vars C
AlmostRingPreserving0: AlmostRingPreserving phi
vs: Vars V
v: V
P1: Pol
w: V
P2: Pol
IH1: eval vs (mulX v P1) = eval vs P1 * vs v
IH2: eval vs (mulX v P2) = eval vs P2 * vs v
(eval vs P1 * vs w + eval vs P2) * vs v + phi 0 =
(eval vs P1 * vs w + eval vs P2) * vs v rewrite (preserves_0 (f:=phi)),plus_0_r.
C: Type
V: Type0
Aplus: canonical_names.Plus C
Amult: canonical_names.Mult C
Azero: canonical_names.Zero C
Aone: canonical_names.One C
Anegate: AlmostNegate C
H: AlmostRing C
H0: DecidablePaths C
Vlt: Relation V
H1: Trichotomy Vlt
R: Type
Aplus0: canonical_names.Plus R
Amult0: canonical_names.Mult R
Azero0: canonical_names.Zero R
Aone0: canonical_names.One R
Anegate0: AlmostNegate R
H2: AlmostRing R
phi: Vars C
AlmostRingPreserving0: AlmostRingPreserving phi
vs: Vars V
v: V
P1: Pol
w: V
P2: Pol
IH1: eval vs (mulX v P1) = eval vs P1 * vs v
IH2: eval vs (mulX v P2) = eval vs P2 * vs v
(eval vs P1 * vs w + eval vs P2) * vs v =
(eval vs P1 * vs w + eval vs P2) * vs v
    reflexivity.
Qed.

Definition mkPX P v Q := add (mulX v P) Q.

Lemma eval_mkPX vs : forall P v Q,
  eval vs (mkPX P v Q) = (eval vs P) * (vs v) + eval vs Q.
C: Type
V: Type0
Aplus: canonical_names.Plus C
Amult: canonical_names.Mult C
Azero: canonical_names.Zero C
Aone: canonical_names.One C
Anegate: AlmostNegate C
H: AlmostRing C
H0: DecidablePaths C
Vlt: Relation V
H1: Trichotomy Vlt
R: Type
Aplus0: canonical_names.Plus R
Amult0: canonical_names.Mult R
Azero0: canonical_names.Zero R
Aone0: canonical_names.One R
Anegate0: AlmostNegate R
H2: AlmostRing R
phi: Vars C
AlmostRingPreserving0: AlmostRingPreserving phi
vs: Vars V
forall (P : Pol) (v : V) (Q : Pol),
eval vs (mkPX P v Q) = eval vs P * vs v + eval vs Q
Proof.
C: Type
V: Type0
Aplus: canonical_names.Plus C
Amult: canonical_names.Mult C
Azero: canonical_names.Zero C
Aone: canonical_names.One C
Anegate: AlmostNegate C
H: AlmostRing C
H0: DecidablePaths C
Vlt: Relation V
H1: Trichotomy Vlt
R: Type
Aplus0: canonical_names.Plus R
Amult0: canonical_names.Mult R
Azero0: canonical_names.Zero R
Aone0: canonical_names.One R
Anegate0: AlmostNegate R
H2: AlmostRing R
phi: Vars C
AlmostRingPreserving0: AlmostRingPreserving phi
vs: Vars V
forall (P : Pol) (v : V) (Q : Pol),
eval vs (mkPX P v Q) = eval vs P * vs v + eval vs Q
intros.
C: Type
V: Type0
Aplus: canonical_names.Plus C
Amult: canonical_names.Mult C
Azero: canonical_names.Zero C
Aone: canonical_names.One C
Anegate: AlmostNegate C
H: AlmostRing C
H0: DecidablePaths C
Vlt: Relation V
H1: Trichotomy Vlt
R: Type
Aplus0: canonical_names.Plus R
Amult0: canonical_names.Mult R
Azero0: canonical_names.Zero R
Aone0: canonical_names.One R
Anegate0: AlmostNegate R
H2: AlmostRing R
phi: Vars C
AlmostRingPreserving0: AlmostRingPreserving phi
vs: Vars V
P: Pol
v: V
Q: Pol
eval vs (mkPX P v Q) = eval vs P * vs v + eval vs Q unfold mkPX.
C: Type
V: Type0
Aplus: canonical_names.Plus C
Amult: canonical_names.Mult C
Azero: canonical_names.Zero C
Aone: canonical_names.One C
Anegate: AlmostNegate C
H: AlmostRing C
H0: DecidablePaths C
Vlt: Relation V
H1: Trichotomy Vlt
R: Type
Aplus0: canonical_names.Plus R
Amult0: canonical_names.Mult R
Azero0: canonical_names.Zero R
Aone0: canonical_names.One R
Anegate0: AlmostNegate R
H2: AlmostRing R
phi: Vars C
AlmostRingPreserving0: AlmostRingPreserving phi
vs: Vars V
P: Pol
v: V
Q: Pol
eval vs (add (mulX v P) Q) =
eval vs P * vs v + eval vs Q
rewrite eval_add,eval_mulX.
C: Type
V: Type0
Aplus: canonical_names.Plus C
Amult: canonical_names.Mult C
Azero: canonical_names.Zero C
Aone: canonical_names.One C
Anegate: AlmostNegate C
H: AlmostRing C
H0: DecidablePaths C
Vlt: Relation V
H1: Trichotomy Vlt
R: Type
Aplus0: canonical_names.Plus R
Amult0: canonical_names.Mult R
Azero0: canonical_names.Zero R
Aone0: canonical_names.One R
Anegate0: AlmostNegate R
H2: AlmostRing R
phi: Vars C
AlmostRingPreserving0: AlmostRingPreserving phi
vs: Vars V
P: Pol
v: V
Q: Pol
eval vs P * vs v + eval vs Q =
eval vs P * vs v + eval vs Q reflexivity.
Qed.

Fixpoint mul P Q :=
  match P, Q with
  | Pconst c, _ => mulC c Q
  | _, Pconst d => mulC d P
  | PX P1 v P2, PX Q1 w Q2 =>
    (* P1 Q1 v w + P1 Q2 v + P2 Q1 w + P2 Q2 *)
    add (mulX v (add (mulX w (mul P1 Q1)) (mul P1 Q2)))
        (add (mulX w (mul P2 Q1)) (mul P2 Q2))
  end.

Lemma eval_mul' vs : forall P Q, eval vs (mul P Q) = eval vs P * eval vs Q.
C: Type
V: Type0
Aplus: canonical_names.Plus C
Amult: canonical_names.Mult C
Azero: canonical_names.Zero C
Aone: canonical_names.One C
Anegate: AlmostNegate C
H: AlmostRing C
H0: DecidablePaths C
Vlt: Relation V
H1: Trichotomy Vlt
R: Type
Aplus0: canonical_names.Plus R
Amult0: canonical_names.Mult R
Azero0: canonical_names.Zero R
Aone0: canonical_names.One R
Anegate0: AlmostNegate R
H2: AlmostRing R
phi: Vars C
AlmostRingPreserving0: AlmostRingPreserving phi
vs: Vars V
forall P Q : Pol,
eval vs (mul P Q) = eval vs P * eval vs Q
Proof.
C: Type
V: Type0
Aplus: canonical_names.Plus C
Amult: canonical_names.Mult C
Azero: canonical_names.Zero C
Aone: canonical_names.One C
Anegate: AlmostNegate C
H: AlmostRing C
H0: DecidablePaths C
Vlt: Relation V
H1: Trichotomy Vlt
R: Type
Aplus0: canonical_names.Plus R
Amult0: canonical_names.Mult R
Azero0: canonical_names.Zero R
Aone0: canonical_names.One R
Anegate0: AlmostNegate R
H2: AlmostRing R
phi: Vars C
AlmostRingPreserving0: AlmostRingPreserving phi
vs: Vars V
forall P Q : Pol,
eval vs (mul P Q) = eval vs P * eval vs Q
induction P as [c | P1 IHP1 v P2 IHP2];[apply eval_mulC|].
C: Type
V: Type0
Aplus: canonical_names.Plus C
Amult: canonical_names.Mult C
Azero: canonical_names.Zero C
Aone: canonical_names.One C
Anegate: AlmostNegate C
H: AlmostRing C
H0: DecidablePaths C
Vlt: Relation V
H1: Trichotomy Vlt
R: Type
Aplus0: canonical_names.Plus R
Amult0: canonical_names.Mult R
Azero0: canonical_names.Zero R
Aone0: canonical_names.One R
Anegate0: AlmostNegate R
H2: AlmostRing R
phi: Vars C
AlmostRingPreserving0: AlmostRingPreserving phi
vs: Vars V
P1: Pol
v: V
P2: Pol
IHP1: forall Q : Pol,
eval vs (mul P1 Q) = eval vs P1 * eval vs Q
IHP2: forall Q : Pol,
eval vs (mul P2 Q) = eval vs P2 * eval vs Q
forall Q : Pol,
eval vs (mul (PX P1 v P2) Q) =
eval vs (PX P1 v P2) * eval vs Q
destruct Q as [d | Q1 w Q2].
C: Type
V: Type0
Aplus: canonical_names.Plus C
Amult: canonical_names.Mult C
Azero: canonical_names.Zero C
Aone: canonical_names.One C
Anegate: AlmostNegate C
H: AlmostRing C
H0: DecidablePaths C
Vlt: Relation V
H1: Trichotomy Vlt
R: Type
Aplus0: canonical_names.Plus R
Amult0: canonical_names.Mult R
Azero0: canonical_names.Zero R
Aone0: canonical_names.One R
Anegate0: AlmostNegate R
H2: AlmostRing R
phi: Vars C
AlmostRingPreserving0: AlmostRingPreserving phi
vs: Vars V
P1: Pol
v: V
P2: Pol
IHP1: forall Q : Pol,
eval vs (mul P1 Q) = eval vs P1 * eval vs Q
IHP2: forall Q : Pol,
eval vs (mul P2 Q) = eval vs P2 * eval vs Q
d: C
eval vs (mul (PX P1 v P2) (Pconst d)) =
eval vs (PX P1 v P2) * eval vs (Pconst d)
C: Type
V: Type0
Aplus: canonical_names.Plus C
Amult: canonical_names.Mult C
Azero: canonical_names.Zero C
Aone: canonical_names.One C
Anegate: AlmostNegate C
H: AlmostRing C
H0: DecidablePaths C
Vlt: Relation V
H1: Trichotomy Vlt
R: Type
Aplus0: canonical_names.Plus R
Amult0: canonical_names.Mult R
Azero0: canonical_names.Zero R
Aone0: canonical_names.One R
Anegate0: AlmostNegate R
H2: AlmostRing R
phi: Vars C
AlmostRingPreserving0: AlmostRingPreserving phi
vs: Vars V
P1: Pol
v: V
P2: Pol
IHP1: forall Q : Pol,
eval vs (mul P1 Q) = eval vs P1 * eval vs Q
IHP2: forall Q : Pol,
eval vs (mul P2 Q) = eval vs P2 * eval vs Q
Q1: Pol
w: V
Q2: Pol
eval vs (mul (PX P1 v P2) (PX Q1 w Q2)) =
eval vs (PX P1 v P2) * eval vs (PX Q1 w Q2)
-
C: Type
V: Type0
Aplus: canonical_names.Plus C
Amult: canonical_names.Mult C
Azero: canonical_names.Zero C
Aone: canonical_names.One C
Anegate: AlmostNegate C
H: AlmostRing C
H0: DecidablePaths C
Vlt: Relation V
H1: Trichotomy Vlt
R: Type
Aplus0: canonical_names.Plus R
Amult0: canonical_names.Mult R
Azero0: canonical_names.Zero R
Aone0: canonical_names.One R
Anegate0: AlmostNegate R
H2: AlmostRing R
phi: Vars C
AlmostRingPreserving0: AlmostRingPreserving phi
vs: Vars V
P1: Pol
v: V
P2: Pol
IHP1: forall Q : Pol,
eval vs (mul P1 Q) = eval vs P1 * eval vs Q
IHP2: forall Q : Pol,
eval vs (mul P2 Q) = eval vs P2 * eval vs Q
d: C
eval vs (mul (PX P1 v P2) (Pconst d)) =
eval vs (PX P1 v P2) * eval vs (Pconst d) change (mul (PX P1 v P2) (Pconst d)) with (mulC d (PX P1 v P2)).
C: Type
V: Type0
Aplus: canonical_names.Plus C
Amult: canonical_names.Mult C
Azero: canonical_names.Zero C
Aone: canonical_names.One C
Anegate: AlmostNegate C
H: AlmostRing C
H0: DecidablePaths C
Vlt: Relation V
H1: Trichotomy Vlt
R: Type
Aplus0: canonical_names.Plus R
Amult0: canonical_names.Mult R
Azero0: canonical_names.Zero R
Aone0: canonical_names.One R
Anegate0: AlmostNegate R
H2: AlmostRing R
phi: Vars C
AlmostRingPreserving0: AlmostRingPreserving phi
vs: Vars V
P1: Pol
v: V
P2: Pol
IHP1: forall Q : Pol,
eval vs (mul P1 Q) = eval vs P1 * eval vs Q
IHP2: forall Q : Pol,
eval vs (mul P2 Q) = eval vs P2 * eval vs Q
d: C
eval vs (mulC d (PX P1 v P2)) =
eval vs (PX P1 v P2) * eval vs (Pconst d)
  rewrite eval_mulC.
C: Type
V: Type0
Aplus: canonical_names.Plus C
Amult: canonical_names.Mult C
Azero: canonical_names.Zero C
Aone: canonical_names.One C
Anegate: AlmostNegate C
H: AlmostRing C
H0: DecidablePaths C
Vlt: Relation V
H1: Trichotomy Vlt
R: Type
Aplus0: canonical_names.Plus R
Amult0: canonical_names.Mult R
Azero0: canonical_names.Zero R
Aone0: canonical_names.One R
Anegate0: AlmostNegate R
H2: AlmostRing R
phi: Vars C
AlmostRingPreserving0: AlmostRingPreserving phi
vs: Vars V
P1: Pol
v: V
P2: Pol
IHP1: forall Q : Pol,
eval vs (mul P1 Q) = eval vs P1 * eval vs Q
IHP2: forall Q : Pol,
eval vs (mul P2 Q) = eval vs P2 * eval vs Q
d: C
phi d * eval vs (PX P1 v P2) =
eval vs (PX P1 v P2) * eval vs (Pconst d) apply mult_comm.
-
C: Type
V: Type0
Aplus: canonical_names.Plus C
Amult: canonical_names.Mult C
Azero: canonical_names.Zero C
Aone: canonical_names.One C
Anegate: AlmostNegate C
H: AlmostRing C
H0: DecidablePaths C
Vlt: Relation V
H1: Trichotomy Vlt
R: Type
Aplus0: canonical_names.Plus R
Amult0: canonical_names.Mult R
Azero0: canonical_names.Zero R
Aone0: canonical_names.One R
Anegate0: AlmostNegate R
H2: AlmostRing R
phi: Vars C
AlmostRingPreserving0: AlmostRingPreserving phi
vs: Vars V
P1: Pol
v: V
P2: Pol
IHP1: forall Q : Pol,
eval vs (mul P1 Q) = eval vs P1 * eval vs Q
IHP2: forall Q : Pol,
eval vs (mul P2 Q) = eval vs P2 * eval vs Q
Q1: Pol
w: V
Q2: Pol
eval vs (mul (PX P1 v P2) (PX Q1 w Q2)) =
eval vs (PX P1 v P2) * eval vs (PX Q1 w Q2) simpl.
C: Type
V: Type0
Aplus: canonical_names.Plus C
Amult: canonical_names.Mult C
Azero: canonical_names.Zero C
Aone: canonical_names.One C
Anegate: AlmostNegate C
H: AlmostRing C
H0: DecidablePaths C
Vlt: Relation V
H1: Trichotomy Vlt
R: Type
Aplus0: canonical_names.Plus R
Amult0: canonical_names.Mult R
Azero0: canonical_names.Zero R
Aone0: canonical_names.One R
Anegate0: AlmostNegate R
H2: AlmostRing R
phi: Vars C
AlmostRingPreserving0: AlmostRingPreserving phi
vs: Vars V
P1: Pol
v: V
P2: Pol
IHP1: forall Q : Pol,
eval vs (mul P1 Q) = eval vs P1 * eval vs Q
IHP2: forall Q : Pol,
eval vs (mul P2 Q) = eval vs P2 * eval vs Q
Q1: Pol
w: V
Q2: Pol
eval vs
  (add (mulX v (add (mulX w (mul P1 Q1)) (mul P1 Q2)))
     (add (mulX w (mul P2 Q1)) (mul P2 Q2))) =
(eval vs P1 * vs v + eval vs P2) *
(eval vs Q1 * vs w + eval vs Q2)
  rewrite plus_mult_distr_r,!plus_mult_distr_l.
C: Type
V: Type0
Aplus: canonical_names.Plus C
Amult: canonical_names.Mult C
Azero: canonical_names.Zero C
Aone: canonical_names.One C
Anegate: AlmostNegate C
H: AlmostRing C
H0: DecidablePaths C
Vlt: Relation V
H1: Trichotomy Vlt
R: Type
Aplus0: canonical_names.Plus R
Amult0: canonical_names.Mult R
Azero0: canonical_names.Zero R
Aone0: canonical_names.One R
Anegate0: AlmostNegate R
H2: AlmostRing R
phi: Vars C
AlmostRingPreserving0: AlmostRingPreserving phi
vs: Vars V
P1: Pol
v: V
P2: Pol
IHP1: forall Q : Pol,
eval vs (mul P1 Q) = eval vs P1 * eval vs Q
IHP2: forall Q : Pol,
eval vs (mul P2 Q) = eval vs P2 * eval vs Q
Q1: Pol
w: V
Q2: Pol
eval vs
  (add (mulX v (add (mulX w (mul P1 Q1)) (mul P1 Q2)))
     (add (mulX w (mul P2 Q1)) (mul P2 Q2))) =
eval vs P1 * vs v * (eval vs Q1 * vs w) +
eval vs P1 * vs v * eval vs Q2 +
eval vs P2 * (eval vs Q1 * vs w + eval vs Q2)
  repeat (rewrite eval_add || rewrite eval_mulX).
C: Type
V: Type0
Aplus: canonical_names.Plus C
Amult: canonical_names.Mult C
Azero: canonical_names.Zero C
Aone: canonical_names.One C
Anegate: AlmostNegate C
H: AlmostRing C
H0: DecidablePaths C
Vlt: Relation V
H1: Trichotomy Vlt
R: Type
Aplus0: canonical_names.Plus R
Amult0: canonical_names.Mult R
Azero0: canonical_names.Zero R
Aone0: canonical_names.One R
Anegate0: AlmostNegate R
H2: AlmostRing R
phi: Vars C
AlmostRingPreserving0: AlmostRingPreserving phi
vs: Vars V
P1: Pol
v: V
P2: Pol
IHP1: forall Q : Pol,
eval vs (mul P1 Q) = eval vs P1 * eval vs Q
IHP2: forall Q : Pol,
eval vs (mul P2 Q) = eval vs P2 * eval vs Q
Q1: Pol
w: V
Q2: Pol
(eval vs (mul P1 Q1) * vs w + eval vs (mul P1 Q2)) *
vs v +
(eval vs (mul P2 Q1) * vs w + eval vs (mul P2 Q2)) =
eval vs P1 * vs v * (eval vs Q1 * vs w) +
eval vs P1 * vs v * eval vs Q2 +
eval vs P2 * (eval vs Q1 * vs w + eval vs Q2)
  rewrite plus_mult_distr_r,(plus_mult_distr_l (eval vs P2)).
C: Type
V: Type0
Aplus: canonical_names.Plus C
Amult: canonical_names.Mult C
Azero: canonical_names.Zero C
Aone: canonical_names.One C
Anegate: AlmostNegate C
H: AlmostRing C
H0: DecidablePaths C
Vlt: Relation V
H1: Trichotomy Vlt
R: Type
Aplus0: canonical_names.Plus R
Amult0: canonical_names.Mult R
Azero0: canonical_names.Zero R
Aone0: canonical_names.One R
Anegate0: AlmostNegate R
H2: AlmostRing R
phi: Vars C
AlmostRingPreserving0: AlmostRingPreserving phi
vs: Vars V
P1: Pol
v: V
P2: Pol
IHP1: forall Q : Pol,
eval vs (mul P1 Q) = eval vs P1 * eval vs Q
IHP2: forall Q : Pol,
eval vs (mul P2 Q) = eval vs P2 * eval vs Q
Q1: Pol
w: V
Q2: Pol
eval vs (mul P1 Q1) * vs w * vs v +
eval vs (mul P1 Q2) * vs v +
(eval vs (mul P2 Q1) * vs w + eval vs (mul P2 Q2)) =
eval vs P1 * vs v * (eval vs Q1 * vs w) +
eval vs P1 * vs v * eval vs Q2 +
(eval vs P2 * (eval vs Q1 * vs w) +
 eval vs P2 * eval vs Q2)
  rewrite IHP1,IHP2.
C: Type
V: Type0
Aplus: canonical_names.Plus C
Amult: canonical_names.Mult C
Azero: canonical_names.Zero C
Aone: canonical_names.One C
Anegate: AlmostNegate C
H: AlmostRing C
H0: DecidablePaths C
Vlt: Relation V
H1: Trichotomy Vlt
R: Type
Aplus0: canonical_names.Plus R
Amult0: canonical_names.Mult R
Azero0: canonical_names.Zero R
Aone0: canonical_names.One R
Anegate0: AlmostNegate R
H2: AlmostRing R
phi: Vars C
AlmostRingPreserving0: AlmostRingPreserving phi
vs: Vars V
P1: Pol
v: V
P2: Pol
IHP1: forall Q : Pol,
eval vs (mul P1 Q) = eval vs P1 * eval vs Q
IHP2: forall Q : Pol,
eval vs (mul P2 Q) = eval vs P2 * eval vs Q
Q1: Pol
w: V
Q2: Pol
eval vs P1 * eval vs Q1 * vs w * vs v +
eval vs (mul P1 Q2) * vs v +
(eval vs P2 * eval vs Q1 * vs w + eval vs (mul P2 Q2)) =
eval vs P1 * vs v * (eval vs Q1 * vs w) +
eval vs P1 * vs v * eval vs Q2 +
(eval vs P2 * (eval vs Q1 * vs w) +
 eval vs P2 * eval vs Q2)
  apply ap011;apply ap011.
C: Type
V: Type0
Aplus: canonical_names.Plus C
Amult: canonical_names.Mult C
Azero: canonical_names.Zero C
Aone: canonical_names.One C
Anegate: AlmostNegate C
H: AlmostRing C
H0: DecidablePaths C
Vlt: Relation V
H1: Trichotomy Vlt
R: Type
Aplus0: canonical_names.Plus R
Amult0: canonical_names.Mult R
Azero0: canonical_names.Zero R
Aone0: canonical_names.One R
Anegate0: AlmostNegate R
H2: AlmostRing R
phi: Vars C
AlmostRingPreserving0: AlmostRingPreserving phi
vs: Vars V
P1: Pol
v: V
P2: Pol
IHP1: forall Q : Pol,
eval vs (mul P1 Q) = eval vs P1 * eval vs Q
IHP2: forall Q : Pol,
eval vs (mul P2 Q) = eval vs P2 * eval vs Q
Q1: Pol
w: V
Q2: Pol
eval vs P1 * eval vs Q1 * vs w * vs v =
eval vs P1 * vs v * (eval vs Q1 * vs w)
C: Type
V: Type0
Aplus: canonical_names.Plus C
Amult: canonical_names.Mult C
Azero: canonical_names.Zero C
Aone: canonical_names.One C
Anegate: AlmostNegate C
H: AlmostRing C
H0: DecidablePaths C
Vlt: Relation V
H1: Trichotomy Vlt
R: Type
Aplus0: canonical_names.Plus R
Amult0: canonical_names.Mult R
Azero0: canonical_names.Zero R
Aone0: canonical_names.One R
Anegate0: AlmostNegate R
H2: AlmostRing R
phi: Vars C
AlmostRingPreserving0: AlmostRingPreserving phi
vs: Vars V
P1: Pol
v: V
P2: Pol
IHP1: forall Q : Pol,
eval vs (mul P1 Q) = eval vs P1 * eval vs Q
IHP2: forall Q : Pol,
eval vs (mul P2 Q) = eval vs P2 * eval vs Q
Q1: Pol
w: V
Q2: Pol
eval vs (mul P1 Q2) * vs v =
eval vs P1 * vs v * eval vs Q2
C: Type
V: Type0
Aplus: canonical_names.Plus C
Amult: canonical_names.Mult C
Azero: canonical_names.Zero C
Aone: canonical_names.One C
Anegate: AlmostNegate C
H: AlmostRing C
H0: DecidablePaths C
Vlt: Relation V
H1: Trichotomy Vlt
R: Type
Aplus0: canonical_names.Plus R
Amult0: canonical_names.Mult R
Azero0: canonical_names.Zero R
Aone0: canonical_names.One R
Anegate0: AlmostNegate R
H2: AlmostRing R
phi: Vars C
AlmostRingPreserving0: AlmostRingPreserving phi
vs: Vars V
P1: Pol
v: V
P2: Pol
IHP1: forall Q : Pol,
eval vs (mul P1 Q) = eval vs P1 * eval vs Q
IHP2: forall Q : Pol,
eval vs (mul P2 Q) = eval vs P2 * eval vs Q
Q1: Pol
w: V
Q2: Pol
eval vs P2 * eval vs Q1 * vs w =
eval vs P2 * (eval vs Q1 * vs w)
C: Type
V: Type0
Aplus: canonical_names.Plus C
Amult: canonical_names.Mult C
Azero: canonical_names.Zero C
Aone: canonical_names.One C
Anegate: AlmostNegate C
H: AlmostRing C
H0: DecidablePaths C
Vlt: Relation V
H1: Trichotomy Vlt
R: Type
Aplus0: canonical_names.Plus R
Amult0: canonical_names.Mult R
Azero0: canonical_names.Zero R
Aone0: canonical_names.One R
Anegate0: AlmostNegate R
H2: AlmostRing R
phi: Vars C
AlmostRingPreserving0: AlmostRingPreserving phi
vs: Vars V
P1: Pol
v: V
P2: Pol
IHP1: forall Q : Pol,
eval vs (mul P1 Q) = eval vs P1 * eval vs Q
IHP2: forall Q : Pol,
eval vs (mul P2 Q) = eval vs P2 * eval vs Q
Q1: Pol
w: V
Q2: Pol
eval vs (mul P2 Q2) = eval vs P2 * eval vs Q2
  +
C: Type
V: Type0
Aplus: canonical_names.Plus C
Amult: canonical_names.Mult C
Azero: canonical_names.Zero C
Aone: canonical_names.One C
Anegate: AlmostNegate C
H: AlmostRing C
H0: DecidablePaths C
Vlt: Relation V
H1: Trichotomy Vlt
R: Type
Aplus0: canonical_names.Plus R
Amult0: canonical_names.Mult R
Azero0: canonical_names.Zero R
Aone0: canonical_names.One R
Anegate0: AlmostNegate R
H2: AlmostRing R
phi: Vars C
AlmostRingPreserving0: AlmostRingPreserving phi
vs: Vars V
P1: Pol
v: V
P2: Pol
IHP1: forall Q : Pol,
eval vs (mul P1 Q) = eval vs P1 * eval vs Q
IHP2: forall Q : Pol,
eval vs (mul P2 Q) = eval vs P2 * eval vs Q
Q1: Pol
w: V
Q2: Pol
eval vs P1 * eval vs Q1 * vs w * vs v =
eval vs P1 * vs v * (eval vs Q1 * vs w) rewrite <-!mult_assoc.
C: Type
V: Type0
Aplus: canonical_names.Plus C
Amult: canonical_names.Mult C
Azero: canonical_names.Zero C
Aone: canonical_names.One C
Anegate: AlmostNegate C
H: AlmostRing C
H0: DecidablePaths C
Vlt: Relation V
H1: Trichotomy Vlt
R: Type
Aplus0: canonical_names.Plus R
Amult0: canonical_names.Mult R
Azero0: canonical_names.Zero R
Aone0: canonical_names.One R
Anegate0: AlmostNegate R
H2: AlmostRing R
phi: Vars C
AlmostRingPreserving0: AlmostRingPreserving phi
vs: Vars V
P1: Pol
v: V
P2: Pol
IHP1: forall Q : Pol,
eval vs (mul P1 Q) = eval vs P1 * eval vs Q
IHP2: forall Q : Pol,
eval vs (mul P2 Q) = eval vs P2 * eval vs Q
Q1: Pol
w: V
Q2: Pol
eval vs P1 * (eval vs Q1 * (vs w * vs v)) =
eval vs P1 * (vs v * (eval vs Q1 * vs w))
    apply ap.
C: Type
V: Type0
Aplus: canonical_names.Plus C
Amult: canonical_names.Mult C
Azero: canonical_names.Zero C
Aone: canonical_names.One C
Anegate: AlmostNegate C
H: AlmostRing C
H0: DecidablePaths C
Vlt: Relation V
H1: Trichotomy Vlt
R: Type
Aplus0: canonical_names.Plus R
Amult0: canonical_names.Mult R
Azero0: canonical_names.Zero R
Aone0: canonical_names.One R
Anegate0: AlmostNegate R
H2: AlmostRing R
phi: Vars C
AlmostRingPreserving0: AlmostRingPreserving phi
vs: Vars V
P1: Pol
v: V
P2: Pol
IHP1: forall Q : Pol,
eval vs (mul P1 Q) = eval vs P1 * eval vs Q
IHP2: forall Q : Pol,
eval vs (mul P2 Q) = eval vs P2 * eval vs Q
Q1: Pol
w: V
Q2: Pol
eval vs Q1 * (vs w * vs v) =
vs v * (eval vs Q1 * vs w)
    rewrite (mult_comm (vs v)).
C: Type
V: Type0
Aplus: canonical_names.Plus C
Amult: canonical_names.Mult C
Azero: canonical_names.Zero C
Aone: canonical_names.One C
Anegate: AlmostNegate C
H: AlmostRing C
H0: DecidablePaths C
Vlt: Relation V
H1: Trichotomy Vlt
R: Type
Aplus0: canonical_names.Plus R
Amult0: canonical_names.Mult R
Azero0: canonical_names.Zero R
Aone0: canonical_names.One R
Anegate0: AlmostNegate R
H2: AlmostRing R
phi: Vars C
AlmostRingPreserving0: AlmostRingPreserving phi
vs: Vars V
P1: Pol
v: V
P2: Pol
IHP1: forall Q : Pol,
eval vs (mul P1 Q) = eval vs P1 * eval vs Q
IHP2: forall Q : Pol,
eval vs (mul P2 Q) = eval vs P2 * eval vs Q
Q1: Pol
w: V
Q2: Pol
eval vs Q1 * (vs w * vs v) = eval vs Q1 * vs w * vs v apply mult_assoc.
  +
C: Type
V: Type0
Aplus: canonical_names.Plus C
Amult: canonical_names.Mult C
Azero: canonical_names.Zero C
Aone: canonical_names.One C
Anegate: AlmostNegate C
H: AlmostRing C
H0: DecidablePaths C
Vlt: Relation V
H1: Trichotomy Vlt
R: Type
Aplus0: canonical_names.Plus R
Amult0: canonical_names.Mult R
Azero0: canonical_names.Zero R
Aone0: canonical_names.One R
Anegate0: AlmostNegate R
H2: AlmostRing R
phi: Vars C
AlmostRingPreserving0: AlmostRingPreserving phi
vs: Vars V
P1: Pol
v: V
P2: Pol
IHP1: forall Q : Pol,
eval vs (mul P1 Q) = eval vs P1 * eval vs Q
IHP2: forall Q : Pol,
eval vs (mul P2 Q) = eval vs P2 * eval vs Q
Q1: Pol
w: V
Q2: Pol
eval vs (mul P1 Q2) * vs v =
eval vs P1 * vs v * eval vs Q2 rewrite <-mult_assoc,(mult_comm (vs v)),mult_assoc.
C: Type
V: Type0
Aplus: canonical_names.Plus C
Amult: canonical_names.Mult C
Azero: canonical_names.Zero C
Aone: canonical_names.One C
Anegate: AlmostNegate C
H: AlmostRing C
H0: DecidablePaths C
Vlt: Relation V
H1: Trichotomy Vlt
R: Type
Aplus0: canonical_names.Plus R
Amult0: canonical_names.Mult R
Azero0: canonical_names.Zero R
Aone0: canonical_names.One R
Anegate0: AlmostNegate R
H2: AlmostRing R
phi: Vars C
AlmostRingPreserving0: AlmostRingPreserving phi
vs: Vars V
P1: Pol
v: V
P2: Pol
IHP1: forall Q : Pol,
eval vs (mul P1 Q) = eval vs P1 * eval vs Q
IHP2: forall Q : Pol,
eval vs (mul P2 Q) = eval vs P2 * eval vs Q
Q1: Pol
w: V
Q2: Pol
eval vs (mul P1 Q2) * vs v =
eval vs P1 * eval vs Q2 * vs v
    rewrite IHP1;reflexivity.
  +
C: Type
V: Type0
Aplus: canonical_names.Plus C
Amult: canonical_names.Mult C
Azero: canonical_names.Zero C
Aone: canonical_names.One C
Anegate: AlmostNegate C
H: AlmostRing C
H0: DecidablePaths C
Vlt: Relation V
H1: Trichotomy Vlt
R: Type
Aplus0: canonical_names.Plus R
Amult0: canonical_names.Mult R
Azero0: canonical_names.Zero R
Aone0: canonical_names.One R
Anegate0: AlmostNegate R
H2: AlmostRing R
phi: Vars C
AlmostRingPreserving0: AlmostRingPreserving phi
vs: Vars V
P1: Pol
v: V
P2: Pol
IHP1: forall Q : Pol,
eval vs (mul P1 Q) = eval vs P1 * eval vs Q
IHP2: forall Q : Pol,
eval vs (mul P2 Q) = eval vs P2 * eval vs Q
Q1: Pol
w: V
Q2: Pol
eval vs P2 * eval vs Q1 * vs w =
eval vs P2 * (eval vs Q1 * vs w) symmetry;apply mult_assoc.
  +
C: Type
V: Type0
Aplus: canonical_names.Plus C
Amult: canonical_names.Mult C
Azero: canonical_names.Zero C
Aone: canonical_names.One C
Anegate: AlmostNegate C
H: AlmostRing C
H0: DecidablePaths C
Vlt: Relation V
H1: Trichotomy Vlt
R: Type
Aplus0: canonical_names.Plus R
Amult0: canonical_names.Mult R
Azero0: canonical_names.Zero R
Aone0: canonical_names.One R
Anegate0: AlmostNegate R
H2: AlmostRing R
phi: Vars C
AlmostRingPreserving0: AlmostRingPreserving phi
vs: Vars V
P1: Pol
v: V
P2: Pol
IHP1: forall Q : Pol,
eval vs (mul P1 Q) = eval vs P1 * eval vs Q
IHP2: forall Q : Pol,
eval vs (mul P2 Q) = eval vs P2 * eval vs Q
Q1: Pol
w: V
Q2: Pol
eval vs (mul P2 Q2) = eval vs P2 * eval vs Q2 auto.
Qed.

Definition eval_mul@{} := ltac:(first [exact eval_mul'@{Ularge}|exact eval_mul'@{}]).

Fixpoint toPol (e: Expr V) :=
  match e with
  | Var v => PX 1 v 0
  | Zero => 0
  | One => 1
  | Plus a b => add (toPol a) (toPol b)
  | Mult a b => mul (toPol a) (toPol b)
  | Neg a => mulC (almost_negate 1) (toPol a)
  end.

Lemma eval_toPol@{} vs : forall e : Expr V,
  eval vs (toPol e) = Quoting.eval _ vs e.
C: Type
V: Type0
Aplus: canonical_names.Plus C
Amult: canonical_names.Mult C
Azero: canonical_names.Zero C
Aone: canonical_names.One C
Anegate: AlmostNegate C
H: AlmostRing C
H0: DecidablePaths C
Vlt: Relation V
H1: Trichotomy Vlt
R: Type
Aplus0: canonical_names.Plus R
Amult0: canonical_names.Mult R
Azero0: canonical_names.Zero R
Aone0: canonical_names.One R
Anegate0: AlmostNegate R
H2: AlmostRing R
phi: Vars C
AlmostRingPreserving0: AlmostRingPreserving phi
vs: Vars V
forall e : Expr V,
eval vs (toPol e) = Quoting.eval R vs e
Proof.
C: Type
V: Type0
Aplus: canonical_names.Plus C
Amult: canonical_names.Mult C
Azero: canonical_names.Zero C
Aone: canonical_names.One C
Anegate: AlmostNegate C
H: AlmostRing C
H0: DecidablePaths C
Vlt: Relation V
H1: Trichotomy Vlt
R: Type
Aplus0: canonical_names.Plus R
Amult0: canonical_names.Mult R
Azero0: canonical_names.Zero R
Aone0: canonical_names.One R
Anegate0: AlmostNegate R
H2: AlmostRing R
phi: Vars C
AlmostRingPreserving0: AlmostRingPreserving phi
vs: Vars V
forall e : Expr V,
eval vs (toPol e) = Quoting.eval R vs e
induction e as [v| | |a IHa b IHb|a IHa b IHb|a IHa];simpl.
C: Type
V: Type0
Aplus: canonical_names.Plus C
Amult: canonical_names.Mult C
Azero: canonical_names.Zero C
Aone: canonical_names.One C
Anegate: AlmostNegate C
H: AlmostRing C
H0: DecidablePaths C
Vlt: Relation V
H1: Trichotomy Vlt
R: Type
Aplus0: canonical_names.Plus R
Amult0: canonical_names.Mult R
Azero0: canonical_names.Zero R
Aone0: canonical_names.One R
Anegate0: AlmostNegate R
H2: AlmostRing R
phi: Vars C
AlmostRingPreserving0: AlmostRingPreserving phi
vs: Vars V
v: V
phi 1 * vs v + phi 0 = vs v
C: Type
V: Type0
Aplus: canonical_names.Plus C
Amult: canonical_names.Mult C
Azero: canonical_names.Zero C
Aone: canonical_names.One C
Anegate: AlmostNegate C
H: AlmostRing C
H0: DecidablePaths C
Vlt: Relation V
H1: Trichotomy Vlt
R: Type
Aplus0: canonical_names.Plus R
Amult0: canonical_names.Mult R
Azero0: canonical_names.Zero R
Aone0: canonical_names.One R
Anegate0: AlmostNegate R
H2: AlmostRing R
phi: Vars C
AlmostRingPreserving0: AlmostRingPreserving phi
vs: Vars V
phi 0 = 0
C: Type
V: Type0
Aplus: canonical_names.Plus C
Amult: canonical_names.Mult C
Azero: canonical_names.Zero C
Aone: canonical_names.One C
Anegate: AlmostNegate C
H: AlmostRing C
H0: DecidablePaths C
Vlt: Relation V
H1: Trichotomy Vlt
R: Type
Aplus0: canonical_names.Plus R
Amult0: canonical_names.Mult R
Azero0: canonical_names.Zero R
Aone0: canonical_names.One R
Anegate0: AlmostNegate R
H2: AlmostRing R
phi: Vars C
AlmostRingPreserving0: AlmostRingPreserving phi
vs: Vars V
phi 1 = 1
C: Type
V: Type0
Aplus: canonical_names.Plus C
Amult: canonical_names.Mult C
Azero: canonical_names.Zero C
Aone: canonical_names.One C
Anegate: AlmostNegate C
H: AlmostRing C
H0: DecidablePaths C
Vlt: Relation V
H1: Trichotomy Vlt
R: Type
Aplus0: canonical_names.Plus R
Amult0: canonical_names.Mult R
Azero0: canonical_names.Zero R
Aone0: canonical_names.One R
Anegate0: AlmostNegate R
H2: AlmostRing R
phi: Vars C
AlmostRingPreserving0: AlmostRingPreserving phi
vs: Vars V
a, b: Expr V
IHa: eval vs (toPol a) = Quoting.eval R vs a
IHb: eval vs (toPol b) = Quoting.eval R vs b
eval vs (add (toPol a) (toPol b)) =
Quoting.eval R vs a + Quoting.eval R vs b
C: Type
V: Type0
Aplus: canonical_names.Plus C
Amult: canonical_names.Mult C
Azero: canonical_names.Zero C
Aone: canonical_names.One C
Anegate: AlmostNegate C
H: AlmostRing C
H0: DecidablePaths C
Vlt: Relation V
H1: Trichotomy Vlt
R: Type
Aplus0: canonical_names.Plus R
Amult0: canonical_names.Mult R
Azero0: canonical_names.Zero R
Aone0: canonical_names.One R
Anegate0: AlmostNegate R
H2: AlmostRing R
phi: Vars C
AlmostRingPreserving0: AlmostRingPreserving phi
vs: Vars V
a, b: Expr V
IHa: eval vs (toPol a) = Quoting.eval R vs a
IHb: eval vs (toPol b) = Quoting.eval R vs b
eval vs (mul (toPol a) (toPol b)) =
Quoting.eval R vs a * Quoting.eval R vs b
C: Type
V: Type0
Aplus: canonical_names.Plus C
Amult: canonical_names.Mult C
Azero: canonical_names.Zero C
Aone: canonical_names.One C
Anegate: AlmostNegate C
H: AlmostRing C
H0: DecidablePaths C
Vlt: Relation V
H1: Trichotomy Vlt
R: Type
Aplus0: canonical_names.Plus R
Amult0: canonical_names.Mult R
Azero0: canonical_names.Zero R
Aone0: canonical_names.One R
Anegate0: AlmostNegate R
H2: AlmostRing R
phi: Vars C
AlmostRingPreserving0: AlmostRingPreserving phi
vs: Vars V
a: Expr V
IHa: eval vs (toPol a) = Quoting.eval R vs a
eval vs (mulC (almost_negate 1) (toPol a)) =
almost_negate (Quoting.eval R vs a)
-
C: Type
V: Type0
Aplus: canonical_names.Plus C
Amult: canonical_names.Mult C
Azero: canonical_names.Zero C
Aone: canonical_names.One C
Anegate: AlmostNegate C
H: AlmostRing C
H0: DecidablePaths C
Vlt: Relation V
H1: Trichotomy Vlt
R: Type
Aplus0: canonical_names.Plus R
Amult0: canonical_names.Mult R
Azero0: canonical_names.Zero R
Aone0: canonical_names.One R
Anegate0: AlmostNegate R
H2: AlmostRing R
phi: Vars C
AlmostRingPreserving0: AlmostRingPreserving phi
vs: Vars V
v: V
phi 1 * vs v + phi 0 = vs v rewrite (preserves_1 (f:=phi)),(preserves_0 (f:=phi)),plus_0_r,mult_1_l.
C: Type
V: Type0
Aplus: canonical_names.Plus C
Amult: canonical_names.Mult C
Azero: canonical_names.Zero C
Aone: canonical_names.One C
Anegate: AlmostNegate C
H: AlmostRing C
H0: DecidablePaths C
Vlt: Relation V
H1: Trichotomy Vlt
R: Type
Aplus0: canonical_names.Plus R
Amult0: canonical_names.Mult R
Azero0: canonical_names.Zero R
Aone0: canonical_names.One R
Anegate0: AlmostNegate R
H2: AlmostRing R
phi: Vars C
AlmostRingPreserving0: AlmostRingPreserving phi
vs: Vars V
v: V
vs v = vs v
  reflexivity.
-
C: Type
V: Type0
Aplus: canonical_names.Plus C
Amult: canonical_names.Mult C
Azero: canonical_names.Zero C
Aone: canonical_names.One C
Anegate: AlmostNegate C
H: AlmostRing C
H0: DecidablePaths C
Vlt: Relation V
H1: Trichotomy Vlt
R: Type
Aplus0: canonical_names.Plus R
Amult0: canonical_names.Mult R
Azero0: canonical_names.Zero R
Aone0: canonical_names.One R
Anegate0: AlmostNegate R
H2: AlmostRing R
phi: Vars C
AlmostRingPreserving0: AlmostRingPreserving phi
vs: Vars V
phi 0 = 0 apply preserves_0.
-
C: Type
V: Type0
Aplus: canonical_names.Plus C
Amult: canonical_names.Mult C
Azero: canonical_names.Zero C
Aone: canonical_names.One C
Anegate: AlmostNegate C
H: AlmostRing C
H0: DecidablePaths C
Vlt: Relation V
H1: Trichotomy Vlt
R: Type
Aplus0: canonical_names.Plus R
Amult0: canonical_names.Mult R
Azero0: canonical_names.Zero R
Aone0: canonical_names.One R
Anegate0: AlmostNegate R
H2: AlmostRing R
phi: Vars C
AlmostRingPreserving0: AlmostRingPreserving phi
vs: Vars V
phi 1 = 1 apply preserves_1.
-
C: Type
V: Type0
Aplus: canonical_names.Plus C
Amult: canonical_names.Mult C
Azero: canonical_names.Zero C
Aone: canonical_names.One C
Anegate: AlmostNegate C
H: AlmostRing C
H0: DecidablePaths C
Vlt: Relation V
H1: Trichotomy Vlt
R: Type
Aplus0: canonical_names.Plus R
Amult0: canonical_names.Mult R
Azero0: canonical_names.Zero R
Aone0: canonical_names.One R
Anegate0: AlmostNegate R
H2: AlmostRing R
phi: Vars C
AlmostRingPreserving0: AlmostRingPreserving phi
vs: Vars V
a, b: Expr V
IHa: eval vs (toPol a) = Quoting.eval R vs a
IHb: eval vs (toPol b) = Quoting.eval R vs b
eval vs (add (toPol a) (toPol b)) =
Quoting.eval R vs a + Quoting.eval R vs b rewrite eval_add,IHa,IHb.
C: Type
V: Type0
Aplus: canonical_names.Plus C
Amult: canonical_names.Mult C
Azero: canonical_names.Zero C
Aone: canonical_names.One C
Anegate: AlmostNegate C
H: AlmostRing C
H0: DecidablePaths C
Vlt: Relation V
H1: Trichotomy Vlt
R: Type
Aplus0: canonical_names.Plus R
Amult0: canonical_names.Mult R
Azero0: canonical_names.Zero R
Aone0: canonical_names.One R
Anegate0: AlmostNegate R
H2: AlmostRing R
phi: Vars C
AlmostRingPreserving0: AlmostRingPreserving phi
vs: Vars V
a, b: Expr V
IHa: eval vs (toPol a) = Quoting.eval R vs a
IHb: eval vs (toPol b) = Quoting.eval R vs b
Quoting.eval R vs a + Quoting.eval R vs b =
Quoting.eval R vs a + Quoting.eval R vs b reflexivity.
-
C: Type
V: Type0
Aplus: canonical_names.Plus C
Amult: canonical_names.Mult C
Azero: canonical_names.Zero C
Aone: canonical_names.One C
Anegate: AlmostNegate C
H: AlmostRing C
H0: DecidablePaths C
Vlt: Relation V
H1: Trichotomy Vlt
R: Type
Aplus0: canonical_names.Plus R
Amult0: canonical_names.Mult R
Azero0: canonical_names.Zero R
Aone0: canonical_names.One R
Anegate0: AlmostNegate R
H2: AlmostRing R
phi: Vars C
AlmostRingPreserving0: AlmostRingPreserving phi
vs: Vars V
a, b: Expr V
IHa: eval vs (toPol a) = Quoting.eval R vs a
IHb: eval vs (toPol b) = Quoting.eval R vs b
eval vs (mul (toPol a) (toPol b)) =
Quoting.eval R vs a * Quoting.eval R vs b rewrite eval_mul,IHa,IHb.
C: Type
V: Type0
Aplus: canonical_names.Plus C
Amult: canonical_names.Mult C
Azero: canonical_names.Zero C
Aone: canonical_names.One C
Anegate: AlmostNegate C
H: AlmostRing C
H0: DecidablePaths C
Vlt: Relation V
H1: Trichotomy Vlt
R: Type
Aplus0: canonical_names.Plus R
Amult0: canonical_names.Mult R
Azero0: canonical_names.Zero R
Aone0: canonical_names.One R
Anegate0: AlmostNegate R
H2: AlmostRing R
phi: Vars C
AlmostRingPreserving0: AlmostRingPreserving phi
vs: Vars V
a, b: Expr V
IHa: eval vs (toPol a) = Quoting.eval R vs a
IHb: eval vs (toPol b) = Quoting.eval R vs b
Quoting.eval R vs a * Quoting.eval R vs b =
Quoting.eval R vs a * Quoting.eval R vs b reflexivity.
-
C: Type
V: Type0
Aplus: canonical_names.Plus C
Amult: canonical_names.Mult C
Azero: canonical_names.Zero C
Aone: canonical_names.One C
Anegate: AlmostNegate C
H: AlmostRing C
H0: DecidablePaths C
Vlt: Relation V
H1: Trichotomy Vlt
R: Type
Aplus0: canonical_names.Plus R
Amult0: canonical_names.Mult R
Azero0: canonical_names.Zero R
Aone0: canonical_names.One R
Anegate0: AlmostNegate R
H2: AlmostRing R
phi: Vars C
AlmostRingPreserving0: AlmostRingPreserving phi
vs: Vars V
a: Expr V
IHa: eval vs (toPol a) = Quoting.eval R vs a
eval vs (mulC (almost_negate 1) (toPol a)) =
almost_negate (Quoting.eval R vs a) rewrite eval_mulC.
C: Type
V: Type0
Aplus: canonical_names.Plus C
Amult: canonical_names.Mult C
Azero: canonical_names.Zero C
Aone: canonical_names.One C
Anegate: AlmostNegate C
H: AlmostRing C
H0: DecidablePaths C
Vlt: Relation V
H1: Trichotomy Vlt
R: Type
Aplus0: canonical_names.Plus R
Amult0: canonical_names.Mult R
Azero0: canonical_names.Zero R
Aone0: canonical_names.One R
Anegate0: AlmostNegate R
H2: AlmostRing R
phi: Vars C
AlmostRingPreserving0: AlmostRingPreserving phi
vs: Vars V
a: Expr V
IHa: eval vs (toPol a) = Quoting.eval R vs a
phi (almost_negate 1) * eval vs (toPol a) =
almost_negate (Quoting.eval R vs a) rewrite (almostring_mor_neg (f:=phi)),preserves_1.
C: Type
V: Type0
Aplus: canonical_names.Plus C
Amult: canonical_names.Mult C
Azero: canonical_names.Zero C
Aone: canonical_names.One C
Anegate: AlmostNegate C
H: AlmostRing C
H0: DecidablePaths C
Vlt: Relation V
H1: Trichotomy Vlt
R: Type
Aplus0: canonical_names.Plus R
Amult0: canonical_names.Mult R
Azero0: canonical_names.Zero R
Aone0: canonical_names.One R
Anegate0: AlmostNegate R
H2: AlmostRing R
phi: Vars C
AlmostRingPreserving0: AlmostRingPreserving phi
vs: Vars V
a: Expr V
IHa: eval vs (toPol a) = Quoting.eval R vs a
almost_negate 1 * eval vs (toPol a) =
almost_negate (Quoting.eval R vs a)
  rewrite <-almost_ring_neg_pr.
C: Type
V: Type0
Aplus: canonical_names.Plus C
Amult: canonical_names.Mult C
Azero: canonical_names.Zero C
Aone: canonical_names.One C
Anegate: AlmostNegate C
H: AlmostRing C
H0: DecidablePaths C
Vlt: Relation V
H1: Trichotomy Vlt
R: Type
Aplus0: canonical_names.Plus R
Amult0: canonical_names.Mult R
Azero0: canonical_names.Zero R
Aone0: canonical_names.One R
Anegate0: AlmostNegate R
H2: AlmostRing R
phi: Vars C
AlmostRingPreserving0: AlmostRingPreserving phi
vs: Vars V
a: Expr V
IHa: eval vs (toPol a) = Quoting.eval R vs a
almost_negate (eval vs (toPol a)) =
almost_negate (Quoting.eval R vs a) apply ap,IHa.
Qed.

End content.