Skip to content
GitLab
Commit 1a3a38de authored by MARCHE Claude's avatar MARCHE Claude
Browse files

clean obsolete Coq files in vacid_0_binary_heaps

parent f3d1ca6d
Hide whitespace changes
Inline Side-by-side
examples/programs/vacid_0_binary_heaps/proofs/elements_Elements_Elements_remove_last_1.v deleted 100644 → 0
View file @ f3d1ca6d
(* This file is generated by Why3's Coq driver *)
(* Beware! Only edit allowed sections below *)
Require Import ZArith.
Require Import Rbase.
Parameter map : forall (a:Type) (b:Type), Type.
Parameter get: forall (a:Type) (b:Type), (map a b) -> a -> b.
Implicit Arguments get.
Parameter set: forall (a:Type) (b:Type), (map a b) -> a -> b -> (map a b).
Implicit Arguments set.
Axiom Select_eq : forall (a:Type) (b:Type), forall (m:(map a b)),
forall (a1:a) (a2:a), forall (b1:b), (a1 = a2) -> ((get (set m a1 b1)
a2) = b1).
Axiom Select_neq : forall (a:Type) (b:Type), forall (m:(map a b)),
forall (a1:a) (a2:a), forall (b1:b), (~ (a1 = a2)) -> ((get (set m a1 b1)
a2) = (get m a2)).
Parameter const: forall (b:Type) (a:Type), b -> (map a b).
Set Contextual Implicit.
Implicit Arguments const.
Unset Contextual Implicit.
Axiom Const : forall (b:Type) (a:Type), forall (b1:b) (a1:a), ((get (const(
b1):(map a b)) a1) = b1).
Definition bag (a:Type) := (map a Z).
Axiom occ_non_negative : forall (a:Type), forall (b:(map a Z)) (x:a),
(0%Z <= (get b x))%Z.
Definition eq_bag (a:Type)(a1:(map a Z)) (b:(map a Z)): Prop := forall (x:a),
((get a1 x) = (get b x)).
Implicit Arguments eq_bag.
Axiom bag_extensionality : forall (a:Type), forall (a1:(map a Z)) (b:(map a
Z)), (eq_bag a1 b) -> (a1 = b).
Parameter empty_bag: forall (a:Type), (map a Z).
Set Contextual Implicit.
Implicit Arguments empty_bag.
Unset Contextual Implicit.
Axiom occ_empty : forall (a:Type), forall (x:a), ((get (empty_bag:(map a Z))
x) = 0%Z).
Axiom is_empty : forall (a:Type), forall (b:(map a Z)), (forall (x:a),
((get b x) = 0%Z)) -> (b = (empty_bag:(map a Z))).
Axiom occ_singleton_eq : forall (a:Type), forall (x:a) (y:a), (x = y) ->
((get (set (empty_bag:(map a Z)) x 1%Z) y) = 1%Z).
Axiom occ_singleton_neq : forall (a:Type), forall (x:a) (y:a), (~ (x = y)) ->
((get (set (empty_bag:(map a Z)) x 1%Z) y) = 0%Z).
Parameter union: forall (a:Type), (map a Z) -> (map a Z) -> (map a Z).
Implicit Arguments union.
Axiom occ_union : forall (a:Type), forall (x:a) (a1:(map a Z)) (b:(map a Z)),
((get (union a1 b) x) = ((get a1 x) + (get b x))%Z).
Axiom Union_comm : forall (a:Type), forall (a1:(map a Z)) (b:(map a Z)),
((union a1 b) = (union b a1)).
Axiom Union_identity : forall (a:Type), forall (a1:(map a Z)), ((union a1
(empty_bag:(map a Z))) = a1).
Axiom Union_assoc : forall (a:Type), forall (a1:(map a Z)) (b:(map a Z))
(c:(map a Z)), ((union a1 (union b c)) = (union (union a1 b) c)).
Axiom bag_simpl : forall (a:Type), forall (a1:(map a Z)) (b:(map a Z))
(c:(map a Z)), ((union a1 b) = (union c b)) -> (a1 = c).
Axiom bag_simpl_left : forall (a:Type), forall (a1:(map a Z)) (b:(map a Z))
(c:(map a Z)), ((union a1 b) = (union a1 c)) -> (b = c).
Definition add (a:Type)(x:a) (b:(map a Z)): (map a Z) :=
(union (set (empty_bag:(map a Z)) x 1%Z) b).
Implicit Arguments add.
Axiom occ_add_eq : forall (a:Type), forall (b:(map a Z)) (x:a) (y:a),
(x = y) -> ((get (add x b) x) = ((get b x) + 1%Z)%Z).
Axiom occ_add_neq : forall (a:Type), forall (b:(map a Z)) (x:a) (y:a),
(~ (x = y)) -> ((get (add x b) y) = (get b y)).
Parameter card: forall (a:Type), (map a Z) -> Z.
Implicit Arguments card.
Axiom Card_empty : forall (a:Type), ((card (empty_bag:(map a Z))) = 0%Z).
Axiom Card_singleton : forall (a:Type), forall (x:a),
((card (set (empty_bag:(map a Z)) x 1%Z)) = 1%Z).
Axiom Card_union : forall (a:Type), forall (x:(map a Z)) (y:(map a Z)),
((card (union x y)) = ((card x) + (card y))%Z).
Axiom Card_zero_empty : forall (a:Type), forall (x:(map a Z)),
((card x) = 0%Z) -> (x = (empty_bag:(map a Z))).
Axiom Max_is_ge : forall (x:Z) (y:Z), (x <= (Zmax x y))%Z /\
(y <= (Zmax x y))%Z.
Axiom Max_is_some : forall (x:Z) (y:Z), ((Zmax x y) = x) \/ ((Zmax x y) = y).
Axiom Min_is_le : forall (x:Z) (y:Z), ((Zmin x y) <= x)%Z /\
((Zmin x y) <= y)%Z.
Axiom Min_is_some : forall (x:Z) (y:Z), ((Zmin x y) = x) \/ ((Zmin x y) = y).
Axiom Max_x : forall (x:Z) (y:Z), (y <= x)%Z -> ((Zmax x y) = x).
Axiom Max_y : forall (x:Z) (y:Z), (x <= y)%Z -> ((Zmax x y) = y).
Axiom Min_x : forall (x:Z) (y:Z), (x <= y)%Z -> ((Zmin x y) = x).
Axiom Min_y : forall (x:Z) (y:Z), (y <= x)%Z -> ((Zmin x y) = y).
Axiom Max_sym : forall (x:Z) (y:Z), (y <= x)%Z -> ((Zmax x y) = (Zmax y x)).
Axiom Min_sym : forall (x:Z) (y:Z), (y <= x)%Z -> ((Zmin x y) = (Zmin y x)).
Parameter diff: forall (a:Type), (map a Z) -> (map a Z) -> (map a Z).
Implicit Arguments diff.
Axiom Diff_occ : forall (a:Type), forall (b1:(map a Z)) (b2:(map a Z)) (x:a),
((get (diff b1 b2) x) = (Zmax 0%Z ((get b1 x) - (get b2 x))%Z)).
Axiom Diff_empty_right : forall (a:Type), forall (b:(map a Z)), ((diff b
(empty_bag:(map a Z))) = b).
Axiom Diff_empty_left : forall (a:Type), forall (b:(map a Z)),
((diff (empty_bag:(map a Z)) b) = (empty_bag:(map a Z))).
Axiom Diff_add : forall (a:Type), forall (b:(map a Z)) (x:a), ((diff (add x
b) (set (empty_bag:(map a Z)) x 1%Z)) = b).
Axiom Diff_comm : forall (a:Type), forall (b:(map a Z)) (b1:(map a Z))
(b2:(map a Z)), ((diff (diff b b1) b2) = (diff (diff b b2) b1)).
Axiom Add_diff : forall (a:Type), forall (b:(map a Z)) (x:a), (0%Z < (get b
x))%Z -> ((add x (diff b (set (empty_bag:(map a Z)) x 1%Z))) = b).
Definition array (a:Type) := (map Z a).
Parameter elements: forall (a:Type), (map Z a) -> Z -> Z -> (map a Z).
Implicit Arguments elements.
Axiom Elements_empty : forall (a:Type), forall (a1:(map Z a)) (i:Z) (j:Z),
(j <= i)%Z -> ((elements a1 i j) = (empty_bag:(map a Z))).
Axiom Elements_singleton : forall (a:Type), forall (a1:(map Z a)) (i:Z)
(j:Z), (j = (i + 1%Z)%Z) -> ((elements a1 i j) = (set (empty_bag:(map a Z))
(get a1 i) 1%Z)).
Axiom Elements_union : forall (a:Type), forall (a1:(map Z a)) (i:Z) (j:Z)
(k:Z), ((i <= j)%Z /\ (j <= k)%Z) -> ((elements a1 i
k) = (union (elements a1 i j) (elements a1 j k))).
(* YOU MAY EDIT THE CONTEXT BELOW *)
(* DO NOT EDIT BELOW *)
Theorem Elements_remove_last : forall (a:Type), forall (a1:(map Z a)) (i:Z)
(j:Z), (i < (j - 1%Z)%Z)%Z -> ((elements a1 i
(j - 1%Z)%Z) = (diff (elements a1 i j) (set (empty_bag:(map a Z)) (get a1
(j - 1%Z)%Z) 1%Z))).
(* YOU MAY EDIT THE PROOF BELOW *)
intros X a i j Hij.
Qed.
(* DO NOT EDIT BELOW *)
examples/programs/vacid_0_binary_heaps/proofs/elements_Elements_Elements_set2_1.v deleted 100644 → 0
View file @ f3d1ca6d
(* This file is generated by Why3's Coq driver *)
(* Beware! Only edit allowed sections below *)
Require Import ZArith.
Require Import Rbase.
Parameter map : forall (a:Type) (b:Type), Type.
Parameter get: forall (a:Type) (b:Type), (map a b) -> a -> b.
Implicit Arguments get.
Parameter set: forall (a:Type) (b:Type), (map a b) -> a -> b -> (map a b).
Implicit Arguments set.
Axiom Select_eq : forall (a:Type) (b:Type), forall (m:(map a b)),
forall (a1:a) (a2:a), forall (b1:b), (a1 = a2) -> ((get (set m a1 b1)
a2) = b1).
Axiom Select_neq : forall (a:Type) (b:Type), forall (m:(map a b)),
forall (a1:a) (a2:a), forall (b1:b), (~ (a1 = a2)) -> ((get (set m a1 b1)
a2) = (get m a2)).
Parameter const: forall (b:Type) (a:Type), b -> (map a b).
Set Contextual Implicit.
Implicit Arguments const.
Unset Contextual Implicit.
Axiom Const : forall (b:Type) (a:Type), forall (b1:b) (a1:a), ((get (const(
b1):(map a b)) a1) = b1).
Definition bag (a:Type) := (map a Z).
Axiom occ_non_negative : forall (a:Type), forall (b:(map a Z)) (x:a),
(0%Z <= (get b x))%Z.
Definition eq_bag (a:Type)(a1:(map a Z)) (b:(map a Z)): Prop := forall (x:a),
((get a1 x) = (get b x)).
Implicit Arguments eq_bag.
Axiom bag_extensionality : forall (a:Type), forall (a1:(map a Z)) (b:(map a
Z)), (eq_bag a1 b) -> (a1 = b).
Parameter empty_bag: forall (a:Type), (map a Z).
Set Contextual Implicit.
Implicit Arguments empty_bag.
Unset Contextual Implicit.
Axiom occ_empty : forall (a:Type), forall (x:a), ((get (empty_bag:(map a Z))
x) = 0%Z).
Axiom is_empty : forall (a:Type), forall (b:(map a Z)), (forall (x:a),
((get b x) = 0%Z)) -> (b = (empty_bag:(map a Z))).
Axiom occ_singleton_eq : forall (a:Type), forall (x:a) (y:a), (x = y) ->
((get (set (empty_bag:(map a Z)) x 1%Z) y) = 1%Z).
Axiom occ_singleton_neq : forall (a:Type), forall (x:a) (y:a), (~ (x = y)) ->
((get (set (empty_bag:(map a Z)) x 1%Z) y) = 0%Z).
Parameter union: forall (a:Type), (map a Z) -> (map a Z) -> (map a Z).
Implicit Arguments union.
Axiom occ_union : forall (a:Type), forall (x:a) (a1:(map a Z)) (b:(map a Z)),
((get (union a1 b) x) = ((get a1 x) + (get b x))%Z).
Axiom Union_comm : forall (a:Type), forall (a1:(map a Z)) (b:(map a Z)),
((union a1 b) = (union b a1)).
Axiom Union_identity : forall (a:Type), forall (a1:(map a Z)), ((union a1
(empty_bag:(map a Z))) = a1).
Axiom Union_assoc : forall (a:Type), forall (a1:(map a Z)) (b:(map a Z))
(c:(map a Z)), ((union a1 (union b c)) = (union (union a1 b) c)).
Axiom bag_simpl : forall (a:Type), forall (a1:(map a Z)) (b:(map a Z))
(c:(map a Z)), ((union a1 b) = (union c b)) -> (a1 = c).
Definition add (a:Type)(x:a) (b:(map a Z)): (map a Z) :=
(union (set (empty_bag:(map a Z)) x 1%Z) b).
Implicit Arguments add.
Axiom occ_add_eq : forall (a:Type), forall (b:(map a Z)) (x:a) (y:a),
(x = y) -> ((get (add x b) x) = ((get b x) + 1%Z)%Z).
Axiom occ_add_neq : forall (a:Type), forall (b:(map a Z)) (x:a) (y:a),
(~ (x = y)) -> ((get (add x b) y) = (get b y)).
Parameter card: forall (a:Type), (map a Z) -> Z.
Implicit Arguments card.
Axiom Card_empty : forall (a:Type), ((card (empty_bag:(map a Z))) = 0%Z).
Axiom Card_singleton : forall (a:Type), forall (x:a),
((card (set (empty_bag:(map a Z)) x 1%Z)) = 1%Z).
Axiom Card_union : forall (a:Type), forall (x:(map a Z)) (y:(map a Z)),
((card (union x y)) = ((card x) + (card y))%Z).
Axiom Card_zero_empty : forall (a:Type), forall (x:(map a Z)),
((card x) = 0%Z) -> (x = (empty_bag:(map a Z))).
Definition array (a:Type) := (map Z a).
Parameter elements: forall (a:Type), (map Z a) -> Z -> Z -> (map a Z).
Implicit Arguments elements.
Axiom Elements_empty : forall (a:Type), forall (a1:(map Z a)) (i:Z) (j:Z),
(j <= i)%Z -> ((elements a1 i j) = (empty_bag:(map a Z))).
Axiom Elements_singleton : forall (a:Type), forall (a1:(map Z a)) (i:Z)
(j:Z), (j = (i + 1%Z)%Z) -> ((elements a1 i j) = (set (empty_bag:(map a Z))
(get a1 i) 1%Z)).
Axiom Elements_union : forall (a:Type), forall (a1:(map Z a)) (i:Z) (j:Z)
(k:Z), ((i <= j)%Z /\ (j <= k)%Z) -> ((elements a1 i
k) = (union (elements a1 i j) (elements a1 j k))).
Axiom Elements_union1 : forall (a:Type), forall (a1:(map Z a)) (i:Z) (j:Z),
(i < j)%Z -> ((elements a1 i j) = (add (get a1 i) (elements a1 (i + 1%Z)%Z
j))).
Axiom Elements_union2 : forall (a:Type), forall (a1:(map Z a)) (i:Z) (j:Z),
(i < j)%Z -> ((elements a1 i j) = (add (get a1 (j - 1%Z)%Z) (elements a1 i
(j - 1%Z)%Z))).
Axiom Elements_set_outside : forall (a:Type), forall (a1:(map Z a)) (i:Z)
(j:Z), (i <= j)%Z -> forall (k:Z), ((k < i)%Z \/ (j <= k)%Z) ->
forall (e:a), ((elements (set a1 k e) i j) = (elements a1 i j)).
Axiom Elements_union3 : forall (a:Type), forall (a1:(map Z a)) (i:Z) (j:Z)
(e:a), (i <= j)%Z -> ((add e (elements a1 i j)) = (elements (set a1 j e) i
(j + 1%Z)%Z)).
(* YOU MAY EDIT THE CONTEXT BELOW *)
(* DO NOT EDIT BELOW *)
Theorem Elements_set2 : forall (a:Type), forall (a1:(map Z a)) (i:Z) (j:Z)
(k:Z), ((i <= k)%Z /\ (k < j)%Z) -> forall (e:a), ((add (get a1 k)
(elements (set a1 k e) i j)) = (add e (elements a1 i j))).
(* YOU MAY EDIT THE PROOF BELOW *)
intros A a i j k Hijk e.
pattern (elements (set a k e) i j);
rewrite Elements_union with (j := k); auto with zarith.
pattern (elements (set a k e) i k);
rewrite Elements_set_outside; auto with zarith.
pattern (elements (set a k e) k j);
rewrite Elements_union1; auto with zarith.
pattern (get (set a k e) k); rewrite Select_eq; auto.
pattern (elements (set a k e) (k + 1) j);
rewrite Elements_set_outside; auto with zarith.
unfold add.
pattern (union (elements a i k)
(union (set empty_bag e 1%Z)
(elements a (k + 1) j)));
rewrite Union_assoc.
pattern (union (elements a i k) (set empty_bag e 1%Z));
rewrite Union_comm.
pattern (union (union (set empty_bag e 1%Z)
(elements a i k))
(elements a (k + 1) j));
rewrite <- Union_assoc.
pattern (union (set empty_bag (get a k) 1%Z)
(union (set empty_bag e 1%Z)
(union (elements a i k) (elements a (k + 1) j)))) ;
rewrite Union_assoc.
pattern (union (set empty_bag (get a k) 1%Z)
(set empty_bag e 1%Z));
rewrite Union_comm.
rewrite <- Union_assoc.
pattern (union (set empty_bag (get a k) 1%Z)
(union (elements a i k) (elements a (k + 1) j)));
rewrite Union_assoc.
pattern (union (set empty_bag (get a k) 1%Z)
(elements a i k));
rewrite Union_comm.
pattern (union (union (elements a i k)
(set empty_bag (get a k) 1%Z))
(elements a (k + 1) j));
rewrite <- Union_assoc.
fold (add (get a k) (elements a (k + 1) j)).
rewrite <- Elements_union1; auto with zarith.
rewrite <- Elements_union; auto with zarith.
Qed.
(* DO NOT EDIT BELOW *)
examples/programs/vacid_0_binary_heaps/proofs/elements_Elements_Elements_set_1.v deleted 100644 → 0
View file @ f3d1ca6d
(* This file is generated by Why3's Coq driver *)
(* Beware! Only edit allowed sections below *)
Require Import ZArith.
Require Import Rbase.
Parameter map : forall (a:Type) (b:Type), Type.
Parameter get: forall (a:Type) (b:Type), (map a b) -> a -> b.
Implicit Arguments get.
Parameter set: forall (a:Type) (b:Type), (map a b) -> a -> b -> (map a b).
Implicit Arguments set.
Axiom Select_eq : forall (a:Type) (b:Type), forall (m:(map a b)),
forall (a1:a) (a2:a), forall (b1:b), (a1 = a2) -> ((get (set m a1 b1)
a2) = b1).
Axiom Select_neq : forall (a:Type) (b:Type), forall (m:(map a b)),
forall (a1:a) (a2:a), forall (b1:b), (~ (a1 = a2)) -> ((get (set m a1 b1)
a2) = (get m a2)).
Parameter const: forall (b:Type) (a:Type), b -> (map a b).
Set Contextual Implicit.
Implicit Arguments const.
Unset Contextual Implicit.
Axiom Const : forall (b:Type) (a:Type), forall (b1:b) (a1:a), ((get (const(
b1):(map a b)) a1) = b1).
Definition bag (a:Type) := (map a Z).
Axiom occ_non_negative : forall (a:Type), forall (b:(map a Z)) (x:a),
(0%Z <= (get b x))%Z.
Definition eq_bag (a:Type)(a1:(map a Z)) (b:(map a Z)): Prop := forall (x:a),
((get a1 x) = (get b x)).
Implicit Arguments eq_bag.
Axiom bag_extensionality : forall (a:Type), forall (a1:(map a Z)) (b:(map a
Z)), (eq_bag a1 b) -> (a1 = b).
Parameter empty_bag: forall (a:Type), (map a Z).
Set Contextual Implicit.
Implicit Arguments empty_bag.
Unset Contextual Implicit.
Axiom occ_empty : forall (a:Type), forall (x:a), ((get (empty_bag:(map a Z))
x) = 0%Z).
Axiom is_empty : forall (a:Type), forall (b:(map a Z)), (forall (x:a),
((get b x) = 0%Z)) -> (b = (empty_bag:(map a Z))).
Axiom occ_singleton_eq : forall (a:Type), forall (x:a) (y:a), (x = y) ->
((get (set (empty_bag:(map a Z)) x 1%Z) y) = 1%Z).
Axiom occ_singleton_neq : forall (a:Type), forall (x:a) (y:a), (~ (x = y)) ->
((get (set (empty_bag:(map a Z)) x 1%Z) y) = 0%Z).
Parameter union: forall (a:Type), (map a Z) -> (map a Z) -> (map a Z).
Implicit Arguments union.
Axiom occ_union : forall (a:Type), forall (x:a) (a1:(map a Z)) (b:(map a Z)),
((get (union a1 b) x) = ((get a1 x) + (get b x))%Z).
Axiom Union_comm : forall (a:Type), forall (a1:(map a Z)) (b:(map a Z)),
((union a1 b) = (union b a1)).
Axiom Union_identity : forall (a:Type), forall (a1:(map a Z)), ((union a1
(empty_bag:(map a Z))) = a1).
Axiom Union_assoc : forall (a:Type), forall (a1:(map a Z)) (b:(map a Z))
(c:(map a Z)), ((union a1 (union b c)) = (union (union a1 b) c)).
Axiom bag_simpl : forall (a:Type), forall (a1:(map a Z)) (b:(map a Z))
(c:(map a Z)), ((union a1 b) = (union c b)) -> (a1 = c).
Definition add (a:Type)(x:a) (b:(map a Z)): (map a Z) :=
(union (set (empty_bag:(map a Z)) x 1%Z) b).
Implicit Arguments add.
Axiom occ_add_eq : forall (a:Type), forall (b:(map a Z)) (x:a) (y:a),
(x = y) -> ((get (add x b) x) = ((get b x) + 1%Z)%Z).
Axiom occ_add_neq : forall (a:Type), forall (b:(map a Z)) (x:a) (y:a),
(~ (x = y)) -> ((get (add x b) y) = (get b y)).
Parameter card: forall (a:Type), (map a Z) -> Z.
Implicit Arguments card.
Axiom Card_empty : forall (a:Type), ((card (empty_bag:(map a Z))) = 0%Z).
Axiom Card_singleton : forall (a:Type), forall (x:a),
((card (set (empty_bag:(map a Z)) x 1%Z)) = 1%Z).
Axiom Card_union : forall (a:Type), forall (x:(map a Z)) (y:(map a Z)),
((card (union x y)) = ((card x) + (card y))%Z).
Axiom Card_zero_empty : forall (a:Type), forall (x:(map a Z)),
((card x) = 0%Z) -> (x = (empty_bag:(map a Z))).
Definition array (a:Type) := (map Z a).
Parameter elements: forall (a:Type), (map Z a) -> Z -> Z -> (map a Z).
Implicit Arguments elements.
Axiom Elements_empty : forall (a:(map Z Z)) (i:Z) (j:Z), (j <= i)%Z ->
((elements a i j) = (empty_bag:(map Z Z))).
Axiom Elements_singleton : forall (a:(map Z Z)) (i:Z) (j:Z),
(j = (i + 1%Z)%Z) -> ((elements a i j) = (set (empty_bag:(map Z Z)) (get a
i) 1%Z)).
Axiom Elements_union : forall (a:(map Z Z)) (i:Z) (j:Z) (k:Z), ((i <= j)%Z /\
(j <= k)%Z) -> ((elements a i k) = (union (elements a i j) (elements a j
k))).
Axiom Elements_union1 : forall (a:(map Z Z)) (i:Z) (j:Z), (i < j)%Z ->
((elements a i j) = (add (get a i) (elements a (i + 1%Z)%Z j))).
Axiom Elements_union2 : forall (a:(map Z Z)) (i:Z) (j:Z), (i < j)%Z ->
((elements a i j) = (add (get a (j - 1%Z)%Z) (elements a i (j - 1%Z)%Z))).
Theorem Elements_set : forall (a:(map Z Z)) (i:Z) (j:Z), (i <= j)%Z ->
forall (k:Z), ((k < i)%Z \/ (j <= k)%Z) -> forall (e:Z), ((elements (set a
k e) i j) = (elements a i j)).
(* YOU MAY EDIT THE PROOF BELOW *)
intros a i.
apply
(Zlt_lower_bound_rec (fun j => forall k : Z,
k < i \/ j <= k -> forall e : Z,
elements (set a k e) i j = elements a i j) i)%Z.
intros j H_induc H_j k H_k e.</