# Library U_prop

``` ```
 Properties of operators on `0,1`
``` Set Implicit Arguments. Set Strict Implicit. Require Import U_base. Require Export Arith. Module Univ_prop (Univ:Universe). Import Univ. Hint Resolve Ueq_refl. Hint Resolve Upos Unit Udiff_0_1 Unth_prop Ueq_le. Hint Resolve Uplus_sym Uplus_assoc Umult_sym Umult_assoc. Hint Resolve Uinv_one Uinv_opp_left Uinv_plus_left. Hint Resolve Uplus_zero_left Umult_one_left Udistr_plus_right Udistr_inv_right. Hint Resolve Uplus_le_compat_right Umult_le_compat_right Uinv_le_compat. Hint Resolve lub_le le_lub lub_eq_mult lub_eq_plus_cte_right. Hint Resolve Ule_total. Hint Immediate Ueq_sym Ule_antisym Ueq_double_neg. Open Scope U_scope. Lemma Ule_0_1 : U0 <= U1. Lemma Ule_refl : forall x:U,(x <= x). Hint Resolve Ule_refl. Lemma Ueq_trans : forall x y z:U, x == y -> y == z -> x == z. Hint Resolve Ueq_trans. Lemma Uplus_eq_compat_right :     forall x y z:U, x == y -> (x + z) == (y + z). Hint Resolve Uplus_eq_compat_right. Lemma Uplus_eq_compat_left :   forall x y z:U, x == y -> (z + x) == (z + y). Lemma Umult_eq_compat_right : forall x y z:U, x == y -> (x * z) == (y * z). Hint Resolve Umult_eq_compat_right. Lemma Umult_eq_compat_left :   forall x y z:U, x == y -> (z * x) == (z * y). Hint Resolve Uplus_eq_compat_left Umult_eq_compat_left. Lemma Uinv_opp_right : forall x, x + Uinv x == U1. Hint Resolve Uinv_opp_right. ```

## Definition of

``` Definition Ult (r1 r2:U) : Prop := ~(r2 <= r1). Infix "<" := Ult : U_scope. Hint Unfold Ult. Lemma Usetoid : Setoid_Theory U Ueq. Add Setoid U Ueq Usetoid. Add Morphism Uplus : Uplus_eq_compat. Add Morphism Umult : Umult_eq_compat. Add Morphism Ule : Ule_eq_compat. Add Morphism Uinv : Uinv_eq_compat. Add Morphism Ult : Ult_eq_compat. ```

### Left normal form with respect to associativity

``` Ltac norm_assoc_left :=      match goal with       | |- context [(Uplus ?X1 (Uplus ?X2 ?X3))]         => (setoid_rewrite (Uplus_assoc X1 X2 X3))      end. Ltac norm_assoc_right :=      match goal with       | |- context [(Uplus (Uplus ?X1 ?X2) ?X3)]         => (setoid_rewrite <- (Uplus_assoc X1 X2 X3))      end. ```

### Properties of

``` Lemma Ule_double_neg :       forall x y, ~~x <= y -> x <= y. Lemma Ule_zero_eq :      forall x, x <= U0 -> x == U0. Lemma Uge_one_eq :      forall x, U1 <= x -> x == U1. Hint Immediate Ule_zero_eq Uge_one_eq. ```

### Properties of

``` Lemma Ult_neq : forall x y:U, x < y -> ~x == y. Lemma Ult_neq_rev : forall x y:U, x < y -> ~y == x. Lemma Ult_le : forall x y:U, x < y -> x <= y. Lemma Ule_diff_lt : forall x y : U,     x <= y -> ~x==y -> x < y. Hint Immediate Ult_neq Ult_neq_rev Ult_le. Hint Resolve Ule_diff_lt. Lemma Udistr_plus_left :     forall x y z:U, (y <= (Uinv z)) -> (x * (y + z)) == (x * y + x * z). Lemma Udistr_inv_left :   forall x y:U, Uinv (x * y) == (x * (Uinv y)) + Uinv x. Hint Resolve Uinv_eq_compat Udistr_plus_left Udistr_inv_left. Lemma Uplus_perm2 : forall x y z : U, x + (y + z) == y + (x + z). Lemma Umult_perm2 : forall x y z : U, x * (y * z) == y * (x * z). Lemma Uplus_perm3 : forall x y z : U, (x + (y + z)) == z + (x + y). Lemma Umult_perm3 : forall x y z : U, (x * (y * z)) == z * (x * y). Hint Resolve Uplus_perm2 Umult_perm2 Uplus_perm3 Umult_perm3. Lemma Uplus_le_compat_left : forall x y z:U, (x <= y) -> (z + x <= z + y). Hint Resolve Uplus_le_compat_left. Lemma Uplus_le_compat : forall x y z t:U, (x <= y) -> (z <= t) -> (x + z <= y + t). Hint Immediate Uplus_le_compat. Lemma Uplus_zero_right : forall x:U, (x + U0) == x. Hint Resolve Uplus_zero_right. Lemma Uinv_zero : (Uinv U0) == U1. Hint Resolve Uinv_zero. Lemma Uinv_inv : forall x : U, Uinv (Uinv x) == x. Hint Resolve Uinv_inv. Lemma Uinv_simpl :   forall x y : U, (Uinv x) == Uinv y -> x == y. Hint Immediate Uinv_simpl. Lemma Umult_le_compat_left :  forall x y z: U, x <= y -> (z * x) <= (z * y). Hint Resolve Umult_le_compat_left. Lemma Umult_one_right : forall x:U, (x * U1) == x. Hint Resolve Umult_one_right. Lemma Uplus_eq_simpl_right : forall x y z:U, (z <= (Uinv x)) -> (z <= (Uinv y)) -> ((x + z) == (y + z)) -> (x == y). Lemma Ule_plus_right : forall x y, (x <= x + y). Lemma Ule_plus_left : forall x y, (y <= x + y). Hint Resolve Ule_plus_right Ule_plus_left. Lemma Ule_mult_right : forall x y, (x * y <= x ). Lemma Ule_mult_left : forall x y, (x * y <= y). Hint Resolve Ule_mult_right Ule_mult_left. Lemma Uinv_le_perm_right :    forall x y:U, (x <= (Uinv y)) -> y <= (Uinv x). Hint Resolve Uinv_le_perm_right. Lemma Uinv_le_perm_left :    forall x y:U, ((Uinv x) <= y) -> (Uinv y) <= x. Hint Resolve Uinv_le_perm_left. Lemma Uinv_eq_perm_left :    forall x y:U, (x == (Uinv y)) -> Uinv x == y. Hint Immediate Uinv_eq_perm_left. Lemma Uinv_eq_perm_right :    forall x y:U, (Uinv x == y) -> x == (Uinv y). Hint Immediate Uinv_eq_perm_right. Lemma Uinv_plus_right :   forall x y, y <= (Uinv x) -> Uinv (x + y) + y == Uinv x. Hint Resolve Uinv_plus_right. Lemma Uplus_eq_simpl_left : forall x y z:U, (x <= (Uinv y)) -> (x <= (Uinv z ))     -> ((x + y) == (x + z)) -> (y == z). Lemma Uplus_eq_zero_left : forall x y:U, (x <= Uinv y) -> (x + y) == y -> x == U0. Lemma Uinv_le_trans : forall x y z t, (x <= Uinv y) -> z<=x -> t<=y -> z<=Uinv t. ```

### disequality

``` Lemma neq_sym : forall x y, ~ (x==y) -> ~y==x. Hint Immediate neq_sym. Lemma Uinv_neq_compat : forall x y, ~ (x == y) -> ~ (Uinv x == Uinv y). Lemma Uinv_neq_simpl : forall x y, ~ (Uinv x == Uinv y) -> ~ (x == y). Hint Resolve Uinv_neq_compat. Hint Immediate Uinv_neq_simpl. Lemma Uinv_neq_left : forall x y, ~ (x == Uinv y) -> ~ (Uinv x == y). Lemma Uinv_neq_right : forall x y, ~ (Uinv x == y) -> ~ (x == Uinv y). ```

### strict order

``` Lemma Ult_antirefl : forall x:U, ~ x < x. Lemma Ult_0_1 : (U0 < U1). Lemma Ule_lt_trans : forall x y z:U, x <= y -> y < z -> x < z. Lemma Ult_le_trans : forall x y z:U, x < y -> y <= z -> x < z. Lemma Ult_trans : forall x y z:U, x < y -> y < z -> x < z. Hint Resolve Ult_0_1 Ult_antirefl. Lemma not_Ult_le : forall x y, ~x < y -> y <= x. Lemma Ule_not_lt : forall x y, x <= y -> ~ y < x. Hint Immediate not_Ult_le Ule_not_lt. Theorem Uplus_le_simpl_left :   forall x y z : U, z <= Uinv x -> z + x <= z + y -> x <= y. Lemma Uplus_lt_compat_right : forall x y z:U, (z <= Uinv y) -> (x < y) -> ((x + z) < (y + z)). Lemma Uplus_lt_compat_left : forall x y z:U, (z <= Uinv y) -> (x < y) -> (z + x < z + y). Hint Resolve Uplus_lt_compat_right Uplus_lt_compat_left. Lemma Uplus_lt_compat : forall x y z t:U, (z <= Uinv x) -> (t <= Uinv y) ->     (x < y) -> (z < t) -> (x + z < y + t). Hint Immediate Uplus_lt_compat. Lemma Uplus_lt_simpl_left : forall x y z:U, (z <= Uinv y) -> (z + x) < (z + y) -> x < y. Lemma Uplus_lt_simpl_right : forall x y z:U, (z <= Uinv y) -> (x + z) < (y + z) -> x < y. Lemma Uplus_one_le : forall x y, x + y == U1 -> Uinv y <= x. Hint Immediate Uplus_one_le. Theorem Uplus_eq_zero :  forall x : U, (x <= Uinv x) -> (x + x) == x -> x == U0. Lemma Umult_zero_left : forall x:U, (U0 * x) == U0. Hint Resolve Umult_zero_left. Lemma Umult_zero_right : forall x:U, (x * U0) == U0. Hint Resolve Uplus_eq_zero Umult_zero_right. ```
 Compatibility of operations with respect to order.
``` Lemma Umult_le_simpl_right :  forall x y z:U, ~(U0 == z) -> (x * z) <= (y * z) -> x <= y. Hint Resolve Umult_le_simpl_right. Lemma Umult_simpl_right :  forall x y z:U, ~(U0 == z) -> (x * z) == (y * z) -> x == y. Lemma Umult_simpl_left :  forall x y z:U, ~(U0 == x) -> (x * y) == (x * z) -> y == z. Lemma Umult_lt_compat_right :  forall x y z:U, ~(U0 == z) -> x < y -> (x * z) < (y * z). Lemma Umult_lt_compat_left :  forall x y z:U, ~(U0 == z) -> x < y -> (z * x) < (z * y). Lemma Umult_lt_simpl_right :  forall x y z:U, ~(U0 == z) -> (x * z) < (y * z) -> x < y. Lemma Umult_lt_simpl_left :  forall x y z:U, ~(U0 == z) -> (z * x) < (z * y) -> x < y. Hint Resolve Umult_lt_compat_left Umult_lt_compat_right.   ```

### More Properties

``` Lemma Uplus_one : forall x y:U,     Uinv x <= y -> x + y == U1. Hint Resolve Uplus_one. Lemma Uplus_one_right : forall x:U, x + U1 == U1. Lemma Uplus_one_left : forall x:U, U1 + x == U1. Hint Resolve Uplus_one_right Uplus_one_left. Lemma Uinv_mult_simpl : forall x y z t,     x <= Uinv y -> (x * z) <= Uinv (y * t). Hint Resolve Uinv_mult_simpl. Lemma Umult_inv_plus :   forall x y, x * Uinv y + y == x + y * Uinv x. Hint Resolve Umult_inv_plus. Lemma Umult_inv_plus_le :   forall x y z, y <= z -> x * Uinv y + y <= x * Uinv z + z. Hint Resolve Umult_inv_plus_le. ```

## Definition of

``` Fixpoint Uexp (x:U) (n:nat) {struct n} : U :=    match n with O => U1 | (S p) => x * Uexp x p end. ```

## Definition of

A conjonction operation which coincides with min and mult on 0 and 1, see Morgan & McIver
``` Definition Uesp (x y:U) := Uinv (Uinv x + Uinv y). Infix "&" := Uesp (left associativity, at level 40) : U_scope. Lemma Uinv_plus_esp :    forall x y, Uinv (x + y) == Uinv x & Uinv y. Hint Resolve Uinv_plus_esp. Lemma Uinv_esp_plus :    forall x y, Uinv (x & y) == Uinv x + Uinv y. Hint Resolve Uinv_esp_plus. Lemma Uesp_sym : forall x y : U, x & y == y & x. Lemma Uesp_one_right : forall x : U, x & U1 == x. Lemma Uesp_zero :    forall x y, x <= Uinv y -> x & y == U0. Hint Resolve Uesp_sym Uesp_one_right Uesp_zero. Lemma Uesp_zero_right : forall x : U, x & U0 == U0. Lemma Uesp_zero_left : forall x : U, U0 & x == U0. Hint Resolve Uesp_zero_right Uesp_zero_left. ```

## Definition of

``` Definition Uminus (x y:U) := Uinv (Uinv x + y). Infix "-" := Uminus : U_scope. Lemma Uminus_le_compat_left :   forall x y z, x <= y -> x - z <= y - z. Lemma Uminus_le_compat_right :   forall x y z, y <= z -> x - z <= x - y. Hint Resolve Uminus_le_compat_left Uminus_le_compat_right. Add Morphism Uminus : Uminus_eq_compat. Hint Immediate Uminus_eq_compat. Lemma Uminus_zero_right : forall x, x - U0 == x. Lemma Uminus_one_left : forall x, U1 - x == Uinv x. Lemma Uminus_le_zero : forall x y, x <= y -> x - y == U0. Hint Resolve Uminus_zero_right Uminus_one_left Uminus_le_zero. Lemma Uminus_plus_simpl :   forall x y, y <= x -> (x - y) + y == x. Lemma Uminus_plus_zero :   forall x y, x <= y -> (x - y) + y == y. Hint Resolve Uminus_plus_simpl Uminus_plus_zero. Lemma Uesp_minus_distr_left :   forall x y z, (x & y) - z == (x - z) & y. Lemma Uesp_minus_distr_right :   forall x y z, (x & y) - z == x & (y - z). Hint Resolve Uesp_minus_distr_left Uesp_minus_distr_right. Lemma Uesp_minus_distr :   forall x y z t, (x & y) - (z + t) == (x - z) & (y - t). Hint Resolve Uesp_minus_distr. ```

## Definition of max

``` Definition max (x y : U) : U := (x - y) + y. Lemma max_le_right : forall x y : U, y <= x -> (max x y) == x. Lemma max_le_left : forall x y : U, x <= y -> (max x y) == y. Hint Resolve max_le_right max_le_left. Lemma max_le_case : forall x y : U, (max x y) == x \/ (max x y) == y. Add Morphism max : max_eq_compat. Lemma Uplus_minus_simpl_right :   forall x y, y <= Uinv x -> (x + y) - y == x. Hint Resolve Uplus_minus_simpl_right. Lemma Uplus_minus_simpl_left :   forall x y, y <= Uinv x -> (x + y) - x == y. Lemma Uminus_assoc_left :   forall x y z, (x - y) - z == x - (y + z). Hint Resolve Uminus_assoc_left. Lemma Uminus_le_perm_left :   forall x y z, y <= x -> x - y <= z -> x <= z + y. Lemma Uplus_le_perm_left :   forall x y z, y <= x -> x <= y + z -> x - y <= z. Lemma Uminus_eq_perm_left :   forall x y z, y <= x -> x - y == z -> x == z + y. Lemma Uplus_eq_perm_left :   forall x y z, y <= Uinv z -> x == y + z -> x - y == z. Hint Resolve Uminus_le_perm_left Uminus_eq_perm_left. Hint Resolve Uplus_le_perm_left Uplus_eq_perm_left. Lemma Uminus_le_perm_right :   forall x y z, z <= y -> x <= y - z -> x + z <= y. Lemma Uplus_le_perm_right :   forall x y z, z <= Uinv x -> x + z <= y -> x <= y - z. Hint Resolve Uminus_le_perm_right Uplus_le_perm_right. Lemma Uminus_le_perm :   forall x y z, z <= y -> x <= Uinv z -> x <= y - z -> z <= y - x. Hint Resolve Uminus_le_perm. Lemma Uminus_eq_perm_right :   forall x y z, z <= y -> x == y - z -> x + z == y. Hint Resolve Uminus_eq_perm_right. Lemma Uminus_zero_le : forall x y, x - y == U0 -> x <= y. Lemma Uminus_lt_non_zero : forall x y, x < y -> ~y - x == U0. Hint Immediate Uminus_zero_le Uminus_lt_non_zero. Lemma Ult_le_nth : forall x y, x < y -> (exists n, x <= y - Unth n). Lemma Uminus_distr_left : forall x y z, (x - y) * z == (x * z) - (y * z). Hint Resolve Uminus_distr_left. Lemma Uminus_distr_right : forall x y z, x * (y - z) == (x * y) - (x * z). Hint Resolve Uminus_distr_right. Lemma Uminus_assoc_right :   forall x y z, y <= x -> z <= y -> x - (y - z) == (x - y) + z. ```

## Properties of generalized sums

``` Definition sigma (alpha : nat -> U) (n:nat) := comp Uplus U0 alpha n. Lemma sigma0 : forall (alpha : nat -> U) (n:nat), sigma alpha 0 = U0. Lemma sigmaS : forall (alpha : nat -> U) (n:nat),     sigma alpha (S n) = (alpha n) + (sigma alpha n). Lemma sigma_incr : forall (f : nat -> U) (n m:nat),  (n <= m)%nat -> (sigma f n) <= (sigma f m). Hint Resolve sigma_incr. Lemma sigma_eq_compat : forall (f g: nat -> U) (n:nat),  (forall k, (k <= n)%nat -> f k == g k) -> (sigma f n) == (sigma g n). Lemma sigma_le_compat : forall (f g: nat -> U) (n:nat),  (forall k, (k <= n)%nat -> f k <= g k) -> (sigma f n) <= (sigma g n). Hint Resolve sigma_eq_compat sigma_le_compat. ```

## Properties of `Unth`

``` Lemma Unth_zero : Unth 0 == U1. Lemma Unth_one : Unth 1 == Uinv (Unth 1). Hint Resolve Unth_zero Unth_one. Lemma Unth_one_plus : Unth 1 + Unth 1 == U1. Hint Resolve Unth_one_plus. Lemma Unth_not_null : forall n, ~(U0 == Unth n). Hint Resolve Unth_not_null. Lemma Unth_prop_sigma : forall n,       Unth n == Uinv (sigma (fun k => Unth n) n). Hint Resolve Unth_prop_sigma. Lemma Unth_sigma_n :   forall n : nat, ~(U1 == sigma (fun k => Unth n) n). Lemma Unth_sigma_Sn :   forall n : nat, U1 == sigma (fun k => Unth n) (S n). Hint Resolve Unth_sigma_n Unth_sigma_Sn. Lemma Unth_decr : forall n, Unth (S n) < Unth n. Hint Resolve Unth_decr. Lemma Unth_le_half : forall n, Unth (S n) <= Unth 1. Hint Resolve Unth_le_half. ```

### mean of two numbers

``` Definition mean (x y:U) := Unth 1 * x + Unth 1 * y. Lemma mean_eq : forall x:U, mean x x ==x. Lemma mean_le_compat_right :   forall x y z, y <= z -> mean x y <= mean x z. Lemma mean_le_compat_left :   forall x y z, x <= y -> mean x z <= mean y z. Hint Resolve mean_eq mean_le_compat_left mean_le_compat_right. Lemma mean_lt_compat_right :   forall x y z, y < z -> mean x y < mean x z. Lemma mean_lt_compat_left :   forall x y z, x < y -> mean x z < mean y z. Hint Resolve mean_eq mean_le_compat_left mean_le_compat_right. Hint Resolve mean_lt_compat_left mean_lt_compat_right. Lemma mean_le_up : forall x y, x <= y -> mean x y <= y. Lemma mean_le_down : forall x y, x <= y -> x <= mean x y. Lemma mean_lt_up : forall x y, x < y -> mean x y < y. Lemma mean_lt_down : forall x y, x < y -> x < mean x y. Hint Resolve mean_le_up mean_le_down mean_lt_up mean_lt_down. Lemma le_half_inv :    forall x, x <= Unth 1 -> x <= Uinv x. Hint Immediate le_half_inv. Lemma ge_half_inv :    forall x, Unth 1 <= x -> Uinv x <= x. Hint Immediate ge_half_inv. Lemma Uinv_le_half_left : forall x, x <= Unth 1 -> Unth 1 <= Uinv x. Lemma Uinv_le_half_right : forall x, Unth 1 <= x -> Uinv x <= Unth 1. Hint Resolve Uinv_le_half_left Uinv_le_half_right. Lemma half_twice : forall x,    (x <= Unth 1) -> (Unth 1) * (x + x) == x. Lemma half_twice_le : forall x, (Unth 1) * (x + x) <= x. Lemma Uinv_half : forall x,  (Unth 1) * (Uinv x) + (Unth 1) == Uinv ((Unth 1) * x). Lemma half_esp : forall x,    (Unth 1 <= x) -> (Unth 1) * (x & x) + Unth 1 == x. Lemma half_esp_le :   forall x, x <= (Unth 1) * (x & x) + Unth 1. Hint Resolve half_esp_le. ```

### Density

``` Lemma Ule_lt_lim :         forall x y, (forall t, t < x -> t <= y) -> x <= y. ```

## Properties of

``` Lemma half_le :    forall x y, y <= Uinv y -> x <= y + y -> (Unth 1) * x <= y. Lemma half_Unth : forall n, (Unth 1)*(Unth n) <= Unth (S n). Hint Resolve half_le half_Unth. Lemma half_exp :    forall n, Uexp (Unth 1) n == Uexp (Unth 1) (S n) + Uexp (Unth 1) (S n). ```

## Properties of least upper bounds

``` Section lubs. Lemma lub_le_stable :    forall f g : nat -> U, (forall n, f n <= g n)     -> lub f <= lub g. Hint Resolve lub_le_stable. Lemma lub_eq_stable :    forall f g, (forall n, f n == g n) -> lub f == lub g. Hint Resolve lub_eq_stable. Lemma lub_zero : (lub (fun n => U0)) == U0. Lemma lub_un : (lub (fun n => U1)) == U1. Lemma lub_cte : forall c:U, (lub (fun n => c)) == c. Hint Resolve lub_zero lub_un lub_cte. Lemma lub_eq_plus_cte_left :    forall (f : nat -> U) (k:U), lub (fun n => k + (f n)) == k + (lub f). Hint Resolve lub_eq_plus_cte_left. Variables f g : nat -> U. Hypothesis monf : (mon_seq Ule f). Hypothesis mong : (mon_seq Ule g). Lemma lub_lift : forall n,     (lub f) == (lub (fun k => f (n+k)%nat)). Hint Resolve lub_lift. Let sum := fun n => f n + g n. Lemma mon_sum : mon_seq Ule sum. Hint Resolve mon_sum. Lemma lub_eq_plus : lub (fun n => (f n) + (g n)) == (lub f) + (lub g). Hint Resolve lub_eq_plus. Variables k : U. Let prod := fun n => k * f n. Lemma mon_prod : mon_seq Ule prod. Let inv:= fun n => Uinv (g n). Lemma lub_inv :    (forall n, f n <= inv n) -> lub f <= Uinv (lub g). End lubs. ```

## Properties of barycentre of two points

``` Section Barycentre. Variables a b : U. Hypothesis sum_le_one : a <= Uinv b. Lemma Uinv_bary :    forall x y : U,    Uinv (a * x + b * y) == a * Uinv x + b * Uinv y + Uinv (a + b). End Barycentre. Lemma sigma_plus :   forall (f g : nat -> U) (n:nat),   (sigma (fun k => (f k) + (g k)) n) == (sigma f n) + (sigma g n). Definition retract (f : nat -> U) :=    forall n, (f n) <= Uinv (sigma f n). Lemma sigma_mult :   forall (f : nat -> U) (n:nat) (c:U),   retract f -> (sigma (fun k => c * (f k)) n) == c * (sigma f n). Hint Resolve sigma_mult. Lemma sigma_prod_maj :  forall (f g : nat -> U),  forall n, (sigma (fun k => (f k) * (g k)) n) <= (sigma f n). Hint Resolve sigma_prod_maj. Lemma sigma_prod_le :  forall (f g : nat -> U) (c:U),  (forall k, (f k) <= c) -> (retract g) ->  forall n, (sigma (fun k => (f k) * (g k)) n) <= c * (sigma g n). Lemma sigma_prod_ge :  forall (f g : nat -> U) (c:U),  (forall k, c <= (f k)) -> (retract g) ->  forall n, c * (sigma g n) <= (sigma (fun k => (f k) * (g k)) n). Hint Resolve sigma_prod_maj sigma_prod_le sigma_prod_ge. Lemma sigma_inv :   forall (f g : nat -> U) (n:nat), (retract f) ->   Uinv (sigma (fun k => (f k) * (g k)) n) ==   (sigma (fun k => (f k) * Uinv (g k)) n) + Uinv (sigma f n). ```

## Product by an integer

``` Definition Nmult (n: nat) (x : U) : U := sigma (fun k => x) n. ```
 Condition for n */ x to be exact
``` Definition Nmult_def (n: nat) (x : U) :=    match n with O => True | S p => x <= Unth p end. Lemma Nmult_def_O : forall x, Nmult_def O x. Hint Resolve Nmult_def_O. Lemma Nmult_def_pred :   forall n x, Nmult_def (S n) x -> Nmult_def n x. Hint Immediate Nmult_def_pred. Hint Unfold Nmult_def. Infix "*/" := Nmult (at level 60) : U_scope. Lemma Nmult_0 : forall (x:U), (0*/x) = U0. Lemma Nmult_S : forall (n:nat) (x:U), (S n*/x) = x + (n*/x). Add Morphism Nmult : Nmult_eq_compat. Lemma Nmult_le_compat_left :    forall (n:nat) (x y:U), (x <= y) -> (n */ x) <= (n */ y). Lemma Nmult_le_compat_right :    forall (n m:nat) (x:U), (n <= m)%nat -> (n */ x) <= (m */ x). Lemma Nmult_Unth_prop :    forall n:nat, Unth n == Uinv (n*/ (Unth n)). Hint Resolve Nmult_Unth_prop. Lemma Nmult_Unth :    forall n:nat, (n*/ Unth n) == Uinv (Unth n). Hint Immediate Nmult_eq_compat. Hint Resolve Nmult_le_compat_left Nmult_le_compat_right Nmult_Unth. Lemma Nmult_Umult_assoc   : forall (n:nat) (x y:U), (Nmult_def n x) -> (n*/(x*y))== (n*/x)*y. ```

## Tactic for simplification of goals

``` Ltac Usimpl :=    match goal with       |- context [(Uplus U0 ?x)] =>                   setoid_rewrite (Uplus_zero_left x)  | |- context [(Uplus ?x U0)] =>                   setoid_rewrite (Uplus_zero_right x)  | |- context [(Uplus U1 ?x)] =>                   setoid_rewrite (Uplus_one_left x)  | |- context [(Uplus ?x U1)] =>                   setoid_rewrite (Uplus_one_right x)  | |- context [(Umult U0 ?x)] =>                   setoid_rewrite (Umult_zero_left x)  | |- context [(Umult ?x U0)] =>                   setoid_rewrite (Umult_zero_right x)  | |- context [(Umult U1 ?x)] =>                   setoid_rewrite (Umult_one_left x)  | |- context [(Umult ?x U1)] =>                   setoid_rewrite (Umult_one_right x)  | |- context [(Uminus U0 ?x)] =>                   setoid_rewrite (Uminus_le_zero U0 x);                   [apply (Upos x)| idtac]  | |- context [(Uminus ?x U0)] =>                   setoid_rewrite (Uminus_zero_right x)  | |- context [(Uminus ?x U1)] =>                   setoid_rewrite (Uminus_le_zero x U1);                   [apply (Unit x)| idtac]  | |- context [(Uinv (Uinv ?x))] =>                   setoid_rewrite (Uinv_inv x)  | |- (Ule (Uplus ?x ?y) (Uplus ?x ?z)) =>                   apply Uplus_le_compat_left  | |- (Ule (Uplus ?x ?z) (Uplus ?y ?z)) =>                   apply Uplus_le_compat_right  | |- (Ule (Uplus ?x ?z) (Uplus ?z ?y)) =>                   setoid_rewrite (Uplus_sym z y); apply Uplus_le_compat_right  | |- (Ule (Uplus ?x ?y) (Uplus ?z ?x)) =>                   setoid_rewrite (Uplus_sym x y); apply Uplus_le_compat_right  | |- (Ueq (Uplus ?x ?y) (Uplus ?x ?z)) =>                   apply Uplus_eq_compat_left  | |- (Ueq (Uplus ?x ?z) (Uplus ?y ?z)) =>                   apply Uplus_eq_compat_right  | |- (Ueq (Uplus ?x ?z) (Uplus ?z ?y)) =>                   setoid_rewrite (Uplus_sym z y); apply Uplus_eq_compat_right  | |- (Ueq (Uplus ?x ?y) (Uplus ?z ?x)) =>                   setoid_rewrite (Uplus_sym x y); apply Uplus_eq_compat_right  | |- (Ule (Umult ?x ?y) (Umult ?x ?z)) =>                   apply Umult_le_compat_left  | |- (Ule (Umult ?x ?z) (Umult ?y ?z)) =>                   apply Umult_le_compat_right  | |- (Ule (Umult ?x ?z) (Umult ?z ?y)) =>                   setoid_rewrite (Umult_sym z y); apply Umult_le_compat_right  | |- (Ule (Umult ?x ?y) (Umult ?z ?x)) =>                   setoid_rewrite (Umult_sym x y); apply Umult_le_compat_right  | |- (Ueq (Umult ?x ?y) (Umult ?x ?z)) =>                   apply Umult_eq_compat_left  | |- (Ueq (Umult ?x ?z) (Umult ?y ?z)) =>                   apply Umult_eq_compat_right  | |- (Ueq (Umult ?x ?z) (Umult ?z ?y)) =>                   setoid_rewrite (Umult_sym z y); apply Umult_eq_compat_right  | |- (Ueq (Umult ?x ?y) (Umult ?z ?x)) =>                   setoid_rewrite (Umult_sym x y); apply Umult_eq_compat_right end. End Univ_prop. ```
This page has been generated by coqdoc