(**************************************************************)
(*   Copyright Dominique Larchey-Wendling [*]                 *)
(*                                                            *)
(*                             [*] Affiliation LORIA -- CNRS  *)
(**************************************************************)
(*      This file is distributed under the terms of the       *)
(*         CeCILL v2 FREE SOFTWARE LICENSE AGREEMENT          *)
(**************************************************************)

Require Import List Permutation Arith Omega.

Require Import utils pos vec. 
Require Import subcode sss mm_defs.
Require Import ill eill.

Set Implicit Arguments.

Local Infix "~p" := (@Permutation _) (at level 70).

(** ** MM reduces to eILL *)

Section Minsky.

  (* We consider Minsky machines with n registers *)

  Variable (n : nat).

  (** register p (0<=p<n) is encoded by p
      its dual            is encoded by n+p

     positions in the program (PC) are encoded from 2*n until (potential) infinity

   **)
   
  Let q (i : nat) : ll_vars := 2*n+i. 
  Let rx (p : pos n) := pos2nat p.
  Let ry (p : pos n) := n+pos2nat p. 

  Let H_rx : forall p q, rx p = rx q -> p = q.
  Proof.
(* Goal: forall (p q : pos n) (_ : @eq nat (rx p) (rx q)), @eq (pos n) p q *)
    intros p1 p2; unfold rx; intros.
(* Goal: @eq (pos n) p1 p2 *)
    apply pos2nat_inj; omega.
  Qed.

  (* This encodes a list of instructions starting at PC=i 

     i:INC x    ~~~>  ((rx x) -o q(1+i)) -o (q i)
     i:DEC x p  ~~~>  (ry x & q p) -o q i and (rx x) -o q(1+i) -o (q i) 

   *)
  
  Local Fixpoint mm_linstr_enc i l :=
    match l with
      | nil          => nil
      | INC x   :: l => LL_INC  (rx x) (q (1+i)) (q i)                                  :: mm_linstr_enc (1+i) l
      | DEC x p :: l => LL_FORK (ry x) (q p)     (q i) :: LL_DEC (rx x) (q (1+i)) (q i) :: mm_linstr_enc (1+i) l
    end.
    
  Local Fact mm_linstr_enc_app i l m : mm_linstr_enc i (l++m) = mm_linstr_enc i l ++ mm_linstr_enc (length l+i) m.
  Proof.
(* Goal: @eq (list eill_cmd) (mm_linstr_enc i (@app (mm_instr n) l m)) (@app eill_cmd (mm_linstr_enc i l) (mm_linstr_enc (Init.Nat.add (@length (mm_instr n) l) i) m)) *)
    revert i; induction l as [ | [ x | x p ] l IHl ]; intros i; simpl; f_equal; auto.
(* Goal: @eq (list eill_cmd) (mm_linstr_enc (S i) (@app (mm_instr n) l m)) (@app eill_cmd (mm_linstr_enc (S i) l) (mm_linstr_enc (S (Init.Nat.add (@length (mm_instr n) l) i)) m)) *)
(* Goal: @eq (list eill_cmd) (@cons eill_cmd (in_ll_cmd_dec (rx x) (q (S i)) (q i)) (mm_linstr_enc (S i) (@app (mm_instr n) l m))) (@cons eill_cmd (in_ll_cmd_dec (rx x) (q (S i)) (q i)) (@app eill_cmd (mm_linstr_enc (S i) l) (mm_linstr_enc (S (Init.Nat.add (@length (mm_instr n) l) i)) m))) *)
    rewrite IHl; do 2 f_equal; omega.
(* Goal: @eq (list eill_cmd) (mm_linstr_enc (S i) (@app (mm_instr n) l m)) (@app eill_cmd (mm_linstr_enc (S i) l) (mm_linstr_enc (S (Init.Nat.add (@length (mm_instr n) l) i)) m)) *)
(* Goal: @eq (list eill_cmd) (@cons eill_cmd (in_ll_cmd_dec (rx x) (q (S i)) (q i)) (mm_linstr_enc (S i) (@app (mm_instr n) l m))) (@cons eill_cmd (in_ll_cmd_dec (rx x) (q (S i)) (q i)) (@app eill_cmd (mm_linstr_enc (S i) l) (mm_linstr_enc (S (Init.Nat.add (@length (mm_instr n) l) i)) m))) *)
    f_equal; rewrite IHl; do 2 f_equal; omega.
  Qed.
    
  Local Fact subcode_mm_linstr_enc i x j l : (i,INC x::nil) <sc (j,l) -> In (LL_INC  (rx x) (q (1+i)) (q i)) (mm_linstr_enc j l).
  Proof.
(* Goal: forall _ : @subcode (mm_instr n) (@pair nat (list (mm_instr n)) i (@cons (mm_instr n) (@mm_dec n x p) (@nil (mm_instr n)))) (@pair nat (list (mm_instr n)) j l), @incl eill_cmd (@cons eill_cmd (in_ll_cmd_fork (ry x) (q p) (q i)) (@cons eill_cmd (in_ll_cmd_dec (rx x) (q (Init.Nat.add (S O) i)) (q i)) (@nil eill_cmd))) (mm_linstr_enc j l) *)
    intros (l1 & l2 & H1 & H2); subst.
(* Goal: @incl eill_cmd (@cons eill_cmd (in_ll_cmd_fork (ry x) (q p) (q (Init.Nat.add j (@length (mm_instr n) l1)))) (@cons eill_cmd (in_ll_cmd_dec (rx x) (q (Init.Nat.add (S O) (Init.Nat.add j (@length (mm_instr n) l1)))) (q (Init.Nat.add j (@length (mm_instr n) l1)))) (@nil eill_cmd))) (mm_linstr_enc j (@app (mm_instr n) l1 (@app (mm_instr n) (@cons (mm_instr n) (@mm_dec n x p) (@nil (mm_instr n))) l2))) *)
    rewrite mm_linstr_enc_app.
(* Goal: @In eill_cmd (in_ll_cmd_inc (rx x) (q (Init.Nat.add (S O) (Init.Nat.add j (@length (mm_instr n) l1)))) (q (Init.Nat.add j (@length (mm_instr n) l1)))) (@app eill_cmd (mm_linstr_enc j l1) (mm_linstr_enc (Init.Nat.add (@length (mm_instr n) l1) j) (@app (mm_instr n) (@cons (mm_instr n) (@mm_inc n x) (@nil (mm_instr n))) l2))) *)
    apply in_or_app; right; left; do 2 f_equal; omega.
  Qed.
  
  Local Fact subcode_mm_linstr_dec i x p j l : (i,DEC x p::nil) <sc (j,l) -> incl (LL_FORK (ry x) (q p) (q i) :: LL_DEC (rx x) (q (1+i)) (q i) :: nil) (mm_linstr_enc j l).
  Proof.
(* Goal: forall _ : @subcode (mm_instr n) (@pair nat (list (mm_instr n)) i (@cons (mm_instr n) (@mm_dec n x p) (@nil (mm_instr n)))) (@pair nat (list (mm_instr n)) j l), @incl eill_cmd (@cons eill_cmd (in_ll_cmd_fork (ry x) (q p) (q i)) (@cons eill_cmd (in_ll_cmd_dec (rx x) (q (Init.Nat.add (S O) i)) (q i)) (@nil eill_cmd))) (mm_linstr_enc j l) *)
    intros (l1 & l2 & H1 & H2); subst.
(* Goal: @incl eill_cmd (@cons eill_cmd (in_ll_cmd_fork (ry x) (q p) (q (Init.Nat.add j (@length (mm_instr n) l1)))) (@cons eill_cmd (in_ll_cmd_dec (rx x) (q (Init.Nat.add (S O) (Init.Nat.add j (@length (mm_instr n) l1)))) (q (Init.Nat.add j (@length (mm_instr n) l1)))) (@nil eill_cmd))) (mm_linstr_enc j (@app (mm_instr n) l1 (@app (mm_instr n) (@cons (mm_instr n) (@mm_dec n x p) (@nil (mm_instr n))) l2))) *)
    rewrite mm_linstr_enc_app.
(* Goal: @incl eill_cmd (@cons eill_cmd (in_ll_cmd_fork (ry x) (q p) (q (Init.Nat.add j (@length (mm_instr n) l1)))) (@cons eill_cmd (in_ll_cmd_dec (rx x) (q (Init.Nat.add (S O) (Init.Nat.add j (@length (mm_instr n) l1)))) (q (Init.Nat.add j (@length (mm_instr n) l1)))) (@nil eill_cmd))) (@app eill_cmd (mm_linstr_enc j l1) (mm_linstr_enc (Init.Nat.add (@length (mm_instr n) l1) j) (@app (mm_instr n) (@cons (mm_instr n) (@mm_dec n x p) (@nil (mm_instr n))) l2))) *)
    intros A HA; apply in_or_app; right.
(* Goal: @In eill_cmd A (mm_linstr_enc (Init.Nat.add (@length (mm_instr n) l1) j) (@app (mm_instr n) (@cons (mm_instr n) (@mm_dec n x p) (@nil (mm_instr n))) l2)) *)
    destruct HA as [ HA | [ HA | [] ] ]; subst.
(* Goal: @In eill_cmd (in_ll_cmd_fork (ry x) (q p) (q (Init.Nat.add j (@length (mm_instr n) l1)))) (mm_linstr_enc (Init.Nat.add (@length (mm_instr n) l1) j) (@app (mm_instr n) (@cons (mm_instr n) (@mm_dec n x p) (@nil (mm_instr n))) l2)) *)
(* Goal: @In eill_cmd (in_ll_cmd_dec (rx x) (q (Init.Nat.add (S O) (Init.Nat.add j (@length (mm_instr n) l1)))) (q (Init.Nat.add j (@length (mm_instr n) l1)))) (mm_linstr_enc (Init.Nat.add (@length (mm_instr n) l1) j) (@app (mm_instr n) (@cons (mm_instr n) (@mm_dec n x p) (@nil (mm_instr n))) l2)) *)
    left; do 2 f_equal; omega.
(* Goal: @In eill_cmd (in_ll_cmd_fork (ry x) (q p) (q (Init.Nat.add j (@length (mm_instr n) l1)))) (mm_linstr_enc (Init.Nat.add (@length (mm_instr n) l1) j) (@app (mm_instr n) (@cons (mm_instr n) (@mm_dec n x p) (@nil (mm_instr n))) l2)) *)
(* Goal: @In eill_cmd (in_ll_cmd_dec (rx x) (q (Init.Nat.add (S O) (Init.Nat.add j (@length (mm_instr n) l1)))) (q (Init.Nat.add j (@length (mm_instr n) l1)))) (mm_linstr_enc (Init.Nat.add (@length (mm_instr n) l1) j) (@app (mm_instr n) (@cons (mm_instr n) (@mm_dec n x p) (@nil (mm_instr n))) l2)) *)
    right; left; do 2 f_equal; omega.
  Qed.
    
  Local Fact mm_linstr_enc_spec i ll A : In A (mm_linstr_enc i ll) -> (exists j x,   (j,INC x::nil)   <sc (i,ll)  /\   A = LL_INC  (rx x) (q (1+j)) (q j))
                                                                   \/ (exists j x p, (j,DEC x p::nil) <sc (i,ll)  /\ ( A = LL_FORK (ry x) (q p)     (q j)
                                                                                                                  \/ A = LL_DEC  (rx x) (q (1+j)) (q j) ) ). 
  Proof.
(* Goal: forall _ : @In eill_cmd A (mm_linstr_enc i ll), or (@ex nat (fun j : nat => @ex (pos n) (fun x : pos n => and (@subcode (mm_instr n) (@pair nat (list (mm_instr n)) j (@cons (mm_instr n) (@mm_inc n x) (@nil (mm_instr n)))) (@pair nat (list (mm_instr n)) i ll)) (@eq eill_cmd A (in_ll_cmd_inc (rx x) (q (Init.Nat.add (S O) j)) (q j)))))) (@ex nat (fun j : nat => @ex (pos n) (fun x : pos n => @ex nat (fun p : nat => and (@subcode (mm_instr n) (@pair nat (list (mm_instr n)) j (@cons (mm_instr n) (@mm_dec n x p) (@nil (mm_instr n)))) (@pair nat (list (mm_instr n)) i ll)) (or (@eq eill_cmd A (in_ll_cmd_fork (ry x) (q p) (q j))) (@eq eill_cmd A (in_ll_cmd_dec (rx x) (q (Init.Nat.add (S O) j)) (q j)))))))) *)
    revert i A; induction ll as [ | [ x | x p ] ll IHll ]; intros i A HA.
(* Goal: or (@ex nat (fun j : nat => @ex (pos n) (fun x : pos n => and (@subcode (mm_instr n) (@pair nat (list (mm_instr n)) j (@cons (mm_instr n) (@mm_inc n x) (@nil (mm_instr n)))) (@pair nat (list (mm_instr n)) i (@nil (mm_instr n)))) (@eq eill_cmd A (in_ll_cmd_inc (rx x) (q (Init.Nat.add (S O) j)) (q j)))))) (@ex nat (fun j : nat => @ex (pos n) (fun x : pos n => @ex nat (fun p : nat => and (@subcode (mm_instr n) (@pair nat (list (mm_instr n)) j (@cons (mm_instr n) (@mm_dec n x p) (@nil (mm_instr n)))) (@pair nat (list (mm_instr n)) i (@nil (mm_instr n)))) (or (@eq eill_cmd A (in_ll_cmd_fork (ry x) (q p) (q j))) (@eq eill_cmd A (in_ll_cmd_dec (rx x) (q (Init.Nat.add (S O) j)) (q j)))))))) *)
(* Goal: or (@ex nat (fun j : nat => @ex (pos n) (fun x0 : pos n => and (@subcode (mm_instr n) (@pair nat (list (mm_instr n)) j (@cons (mm_instr n) (@mm_inc n x0) (@nil (mm_instr n)))) (@pair nat (list (mm_instr n)) i (@cons (mm_instr n) (@mm_inc n x) ll))) (@eq eill_cmd A (in_ll_cmd_inc (rx x0) (q (Init.Nat.add (S O) j)) (q j)))))) (@ex nat (fun j : nat => @ex (pos n) (fun x0 : pos n => @ex nat (fun p : nat => and (@subcode (mm_instr n) (@pair nat (list (mm_instr n)) j (@cons (mm_instr n) (@mm_dec n x0 p) (@nil (mm_instr n)))) (@pair nat (list (mm_instr n)) i (@cons (mm_instr n) (@mm_inc n x) ll))) (or (@eq eill_cmd A (in_ll_cmd_fork (ry x0) (q p) (q j))) (@eq eill_cmd A (in_ll_cmd_dec (rx x0) (q (Init.Nat.add (S O) j)) (q j)))))))) *)
(* Goal: or (@ex nat (fun j : nat => @ex (pos n) (fun x0 : pos n => and (@subcode (mm_instr n) (@pair nat (list (mm_instr n)) j (@cons (mm_instr n) (@mm_inc n x0) (@nil (mm_instr n)))) (@pair nat (list (mm_instr n)) i (@cons (mm_instr n) (@mm_dec n x p) ll))) (@eq eill_cmd A (in_ll_cmd_inc (rx x0) (q (Init.Nat.add (S O) j)) (q j)))))) (@ex nat (fun j : nat => @ex (pos n) (fun x0 : pos n => @ex nat (fun p0 : nat => and (@subcode (mm_instr n) (@pair nat (list (mm_instr n)) j (@cons (mm_instr n) (@mm_dec n x0 p0) (@nil (mm_instr n)))) (@pair nat (list (mm_instr n)) i (@cons (mm_instr n) (@mm_dec n x p) ll))) (or (@eq eill_cmd A (in_ll_cmd_fork (ry x0) (q p0) (q j))) (@eq eill_cmd A (in_ll_cmd_dec (rx x0) (q (Init.Nat.add (S O) j)) (q j)))))))) *)
    destruct HA.
(* Goal: or (@ex nat (fun j : nat => @ex (pos n) (fun x0 : pos n => and (@subcode (mm_instr n) (@pair nat (list (mm_instr n)) j (@cons (mm_instr n) (@mm_inc n x0) (@nil (mm_instr n)))) (@pair nat (list (mm_instr n)) i (@cons (mm_instr n) (@mm_dec n x p) ll))) (@eq eill_cmd A (in_ll_cmd_inc (rx x0) (q (Init.Nat.add (S O) j)) (q j)))))) (@ex nat (fun j : nat => @ex (pos n) (fun x0 : pos n => @ex nat (fun p0 : nat => and (@subcode (mm_instr n) (@pair nat (list (mm_instr n)) j (@cons (mm_instr n) (@mm_dec n x0 p0) (@nil (mm_instr n)))) (@pair nat (list (mm_instr n)) i (@cons (mm_instr n) (@mm_dec n x p) ll))) (or (@eq eill_cmd A (in_ll_cmd_fork (ry x0) (q p0) (q j))) (@eq eill_cmd A (in_ll_cmd_dec (rx x0) (q (Init.Nat.add (S O) j)) (q j)))))))) *)
    destruct HA as [ HA | HA ].
(* Goal: or (@ex nat (fun j : nat => @ex (pos n) (fun x0 : pos n => and (@subcode (mm_instr n) (@pair nat (list (mm_instr n)) j (@cons (mm_instr n) (@mm_inc n x0) (@nil (mm_instr n)))) (@pair nat (list (mm_instr n)) i (@cons (mm_instr n) (@mm_inc n x) ll))) (@eq eill_cmd A (in_ll_cmd_inc (rx x0) (q (Init.Nat.add (S O) j)) (q j)))))) (@ex nat (fun j : nat => @ex (pos n) (fun x0 : pos n => @ex nat (fun p : nat => and (@subcode (mm_instr n) (@pair nat (list (mm_instr n)) j (@cons (mm_instr n) (@mm_dec n x0 p) (@nil (mm_instr n)))) (@pair nat (list (mm_instr n)) i (@cons (mm_instr n) (@mm_inc n x) ll))) (or (@eq eill_cmd A (in_ll_cmd_fork (ry x0) (q p) (q j))) (@eq eill_cmd A (in_ll_cmd_dec (rx x0) (q (Init.Nat.add (S O) j)) (q j)))))))) *)
(* Goal: or (@ex nat (fun j : nat => @ex (pos n) (fun x0 : pos n => and (@subcode (mm_instr n) (@pair nat (list (mm_instr n)) j (@cons (mm_instr n) (@mm_inc n x0) (@nil (mm_instr n)))) (@pair nat (list (mm_instr n)) i (@cons (mm_instr n) (@mm_inc n x) ll))) (@eq eill_cmd A (in_ll_cmd_inc (rx x0) (q (Init.Nat.add (S O) j)) (q j)))))) (@ex nat (fun j : nat => @ex (pos n) (fun x0 : pos n => @ex nat (fun p : nat => and (@subcode (mm_instr n) (@pair nat (list (mm_instr n)) j (@cons (mm_instr n) (@mm_dec n x0 p) (@nil (mm_instr n)))) (@pair nat (list (mm_instr n)) i (@cons (mm_instr n) (@mm_inc n x) ll))) (or (@eq eill_cmd A (in_ll_cmd_fork (ry x0) (q p) (q j))) (@eq eill_cmd A (in_ll_cmd_dec (rx x0) (q (Init.Nat.add (S O) j)) (q j)))))))) *)
(* Goal: or (@ex nat (fun j : nat => @ex (pos n) (fun x0 : pos n => and (@subcode (mm_instr n) (@pair nat (list (mm_instr n)) j (@cons (mm_instr n) (@mm_inc n x0) (@nil (mm_instr n)))) (@pair nat (list (mm_instr n)) i (@cons (mm_instr n) (@mm_dec n x p) ll))) (@eq eill_cmd A (in_ll_cmd_inc (rx x0) (q (Init.Nat.add (S O) j)) (q j)))))) (@ex nat (fun j : nat => @ex (pos n) (fun x0 : pos n => @ex nat (fun p0 : nat => and (@subcode (mm_instr n) (@pair nat (list (mm_instr n)) j (@cons (mm_instr n) (@mm_dec n x0 p0) (@nil (mm_instr n)))) (@pair nat (list (mm_instr n)) i (@cons (mm_instr n) (@mm_dec n x p) ll))) (or (@eq eill_cmd A (in_ll_cmd_fork (ry x0) (q p0) (q j))) (@eq eill_cmd A (in_ll_cmd_dec (rx x0) (q (Init.Nat.add (S O) j)) (q j)))))))) *)
    left; exists i, x; split; auto.
(* Goal: or (@ex nat (fun j : nat => @ex (pos n) (fun x0 : pos n => and (@subcode (mm_instr n) (@pair nat (list (mm_instr n)) j (@cons (mm_instr n) (@mm_inc n x0) (@nil (mm_instr n)))) (@pair nat (list (mm_instr n)) i (@cons (mm_instr n) (@mm_dec n x p) ll))) (@eq eill_cmd A (in_ll_cmd_inc (rx x0) (q (Init.Nat.add (S O) j)) (q j)))))) (@ex nat (fun j : nat => @ex (pos n) (fun x0 : pos n => @ex nat (fun p0 : nat => and (@subcode (mm_instr n) (@pair nat (list (mm_instr n)) j (@cons (mm_instr n) (@mm_dec n x0 p0) (@nil (mm_instr n)))) (@pair nat (list (mm_instr n)) i (@cons (mm_instr n) (@mm_dec n x p) ll))) (or (@eq eill_cmd A (in_ll_cmd_fork (ry x0) (q p0) (q j))) (@eq eill_cmd A (in_ll_cmd_dec (rx x0) (q (Init.Nat.add (S O) j)) (q j)))))))) *)
    apply IHll in HA.
(* Goal: or (@ex nat (fun j : nat => @ex (pos n) (fun x0 : pos n => and (@subcode (mm_instr n) (@pair nat (list (mm_instr n)) j (@cons (mm_instr n) (@mm_inc n x0) (@nil (mm_instr n)))) (@pair nat (list (mm_instr n)) i (@cons (mm_instr n) (@mm_inc n x) ll))) (@eq eill_cmd A (in_ll_cmd_inc (rx x0) (q (Init.Nat.add (S O) j)) (q j)))))) (@ex nat (fun j : nat => @ex (pos n) (fun x0 : pos n => @ex nat (fun p : nat => and (@subcode (mm_instr n) (@pair nat (list (mm_instr n)) j (@cons (mm_instr n) (@mm_dec n x0 p) (@nil (mm_instr n)))) (@pair nat (list (mm_instr n)) i (@cons (mm_instr n) (@mm_inc n x) ll))) (or (@eq eill_cmd A (in_ll_cmd_fork (ry x0) (q p) (q j))) (@eq eill_cmd A (in_ll_cmd_dec (rx x0) (q (Init.Nat.add (S O) j)) (q j)))))))) *)
(* Goal: or (@ex nat (fun j : nat => @ex (pos n) (fun x0 : pos n => and (@subcode (mm_instr n) (@pair nat (list (mm_instr n)) j (@cons (mm_instr n) (@mm_inc n x0) (@nil (mm_instr n)))) (@pair nat (list (mm_instr n)) i (@cons (mm_instr n) (@mm_dec n x p) ll))) (@eq eill_cmd A (in_ll_cmd_inc (rx x0) (q (Init.Nat.add (S O) j)) (q j)))))) (@ex nat (fun j : nat => @ex (pos n) (fun x0 : pos n => @ex nat (fun p0 : nat => and (@subcode (mm_instr n) (@pair nat (list (mm_instr n)) j (@cons (mm_instr n) (@mm_dec n x0 p0) (@nil (mm_instr n)))) (@pair nat (list (mm_instr n)) i (@cons (mm_instr n) (@mm_dec n x p) ll))) (or (@eq eill_cmd A (in_ll_cmd_fork (ry x0) (q p0) (q j))) (@eq eill_cmd A (in_ll_cmd_dec (rx x0) (q (Init.Nat.add (S O) j)) (q j)))))))) *)
    destruct HA as [ (j & x' & H1 & H2) | (j & x' & p & H1 & H2) ].
(* Goal: or (@ex nat (fun j : nat => @ex (pos n) (fun x0 : pos n => and (@subcode (mm_instr n) (@pair nat (list (mm_instr n)) j (@cons (mm_instr n) (@mm_inc n x0) (@nil (mm_instr n)))) (@pair nat (list (mm_instr n)) i (@cons (mm_instr n) (@mm_dec n x p) ll))) (@eq eill_cmd A (in_ll_cmd_inc (rx x0) (q (Init.Nat.add (S O) j)) (q j)))))) (@ex nat (fun j : nat => @ex (pos n) (fun x0 : pos n => @ex nat (fun p0 : nat => and (@subcode (mm_instr n) (@pair nat (list (mm_instr n)) j (@cons (mm_instr n) (@mm_dec n x0 p0) (@nil (mm_instr n)))) (@pair nat (list (mm_instr n)) i (@cons (mm_instr n) (@mm_dec n x p) ll))) (or (@eq eill_cmd A (in_ll_cmd_fork (ry x0) (q p0) (q j))) (@eq eill_cmd A (in_ll_cmd_dec (rx x0) (q (Init.Nat.add (S O) j)) (q j)))))))) *)
(* Goal: or (@ex nat (fun j : nat => @ex (pos n) (fun x0 : pos n => and (@subcode (mm_instr n) (@pair nat (list (mm_instr n)) j (@cons (mm_instr n) (@mm_inc n x0) (@nil (mm_instr n)))) (@pair nat (list (mm_instr n)) i (@cons (mm_instr n) (@mm_dec n x p) ll))) (@eq eill_cmd A (in_ll_cmd_inc (rx x0) (q (Init.Nat.add (S O) j)) (q j)))))) (@ex nat (fun j : nat => @ex (pos n) (fun x0 : pos n => @ex nat (fun p0 : nat => and (@subcode (mm_instr n) (@pair nat (list (mm_instr n)) j (@cons (mm_instr n) (@mm_dec n x0 p0) (@nil (mm_instr n)))) (@pair nat (list (mm_instr n)) i (@cons (mm_instr n) (@mm_dec n x p) ll))) (or (@eq eill_cmd A (in_ll_cmd_fork (ry x0) (q p0) (q j))) (@eq eill_cmd A (in_ll_cmd_dec (rx x0) (q (Init.Nat.add (S O) j)) (q j)))))))) *)
    left; exists j, x'; split; auto.
(* Goal: @subcode (mm_instr n) (@pair nat (list (mm_instr n)) j (@cons (mm_instr n) (@mm_dec n x' p') (@nil (mm_instr n)))) (@pair nat (list (mm_instr n)) i (@cons (mm_instr n) (@mm_dec n x p) ll)) *)
    apply subcode_trans with (1 := H1); subcode_tac; solve list eq.
(* Goal: or (@ex nat (fun j : nat => @ex (pos n) (fun x0 : pos n => and (@subcode (mm_instr n) (@pair nat (list (mm_instr n)) j (@cons (mm_instr n) (@mm_inc n x0) (@nil (mm_instr n)))) (@pair nat (list (mm_instr n)) i (@cons (mm_instr n) (@mm_inc n x) ll))) (@eq eill_cmd A (in_ll_cmd_inc (rx x0) (q (Init.Nat.add (S O) j)) (q j)))))) (@ex nat (fun j : nat => @ex (pos n) (fun x0 : pos n => @ex nat (fun p : nat => and (@subcode (mm_instr n) (@pair nat (list (mm_instr n)) j (@cons (mm_instr n) (@mm_dec n x0 p) (@nil (mm_instr n)))) (@pair nat (list (mm_instr n)) i (@cons (mm_instr n) (@mm_inc n x) ll))) (or (@eq eill_cmd A (in_ll_cmd_fork (ry x0) (q p) (q j))) (@eq eill_cmd A (in_ll_cmd_dec (rx x0) (q (Init.Nat.add (S O) j)) (q j)))))))) *)
(* Goal: or (@ex nat (fun j : nat => @ex (pos n) (fun x0 : pos n => and (@subcode (mm_instr n) (@pair nat (list (mm_instr n)) j (@cons (mm_instr n) (@mm_inc n x0) (@nil (mm_instr n)))) (@pair nat (list (mm_instr n)) i (@cons (mm_instr n) (@mm_dec n x p) ll))) (@eq eill_cmd A (in_ll_cmd_inc (rx x0) (q (Init.Nat.add (S O) j)) (q j)))))) (@ex nat (fun j : nat => @ex (pos n) (fun x0 : pos n => @ex nat (fun p0 : nat => and (@subcode (mm_instr n) (@pair nat (list (mm_instr n)) j (@cons (mm_instr n) (@mm_dec n x0 p0) (@nil (mm_instr n)))) (@pair nat (list (mm_instr n)) i (@cons (mm_instr n) (@mm_dec n x p) ll))) (or (@eq eill_cmd A (in_ll_cmd_fork (ry x0) (q p0) (q j))) (@eq eill_cmd A (in_ll_cmd_dec (rx x0) (q (Init.Nat.add (S O) j)) (q j)))))))) *)
    right; exists j, x', p; split; auto.
(* Goal: @subcode (mm_instr n) (@pair nat (list (mm_instr n)) j (@cons (mm_instr n) (@mm_dec n x' p') (@nil (mm_instr n)))) (@pair nat (list (mm_instr n)) i (@cons (mm_instr n) (@mm_dec n x p) ll)) *)
    apply subcode_trans with (1 := H1); subcode_tac; solve list eq.
(* Goal: or (@ex nat (fun j : nat => @ex (pos n) (fun x0 : pos n => and (@subcode (mm_instr n) (@pair nat (list (mm_instr n)) j (@cons (mm_instr n) (@mm_inc n x0) (@nil (mm_instr n)))) (@pair nat (list (mm_instr n)) i (@cons (mm_instr n) (@mm_dec n x p) ll))) (@eq eill_cmd A (in_ll_cmd_inc (rx x0) (q (Init.Nat.add (S O) j)) (q j)))))) (@ex nat (fun j : nat => @ex (pos n) (fun x0 : pos n => @ex nat (fun p0 : nat => and (@subcode (mm_instr n) (@pair nat (list (mm_instr n)) j (@cons (mm_instr n) (@mm_dec n x0 p0) (@nil (mm_instr n)))) (@pair nat (list (mm_instr n)) i (@cons (mm_instr n) (@mm_dec n x p) ll))) (or (@eq eill_cmd A (in_ll_cmd_fork (ry x0) (q p0) (q j))) (@eq eill_cmd A (in_ll_cmd_dec (rx x0) (q (Init.Nat.add (S O) j)) (q j)))))))) *)
    destruct HA as [ HA | HA ].
(* Goal: or (@ex nat (fun j : nat => @ex (pos n) (fun x0 : pos n => and (@subcode (mm_instr n) (@pair nat (list (mm_instr n)) j (@cons (mm_instr n) (@mm_inc n x0) (@nil (mm_instr n)))) (@pair nat (list (mm_instr n)) i (@cons (mm_instr n) (@mm_dec n x p) ll))) (@eq eill_cmd A (in_ll_cmd_inc (rx x0) (q (Init.Nat.add (S O) j)) (q j)))))) (@ex nat (fun j : nat => @ex (pos n) (fun x0 : pos n => @ex nat (fun p0 : nat => and (@subcode (mm_instr n) (@pair nat (list (mm_instr n)) j (@cons (mm_instr n) (@mm_dec n x0 p0) (@nil (mm_instr n)))) (@pair nat (list (mm_instr n)) i (@cons (mm_instr n) (@mm_dec n x p) ll))) (or (@eq eill_cmd A (in_ll_cmd_fork (ry x0) (q p0) (q j))) (@eq eill_cmd A (in_ll_cmd_dec (rx x0) (q (Init.Nat.add (S O) j)) (q j)))))))) *)
(* Goal: or (@ex nat (fun j : nat => @ex (pos n) (fun x0 : pos n => and (@subcode (mm_instr n) (@pair nat (list (mm_instr n)) j (@cons (mm_instr n) (@mm_inc n x0) (@nil (mm_instr n)))) (@pair nat (list (mm_instr n)) i (@cons (mm_instr n) (@mm_dec n x p) ll))) (@eq eill_cmd A (in_ll_cmd_inc (rx x0) (q (Init.Nat.add (S O) j)) (q j)))))) (@ex nat (fun j : nat => @ex (pos n) (fun x0 : pos n => @ex nat (fun p0 : nat => and (@subcode (mm_instr n) (@pair nat (list (mm_instr n)) j (@cons (mm_instr n) (@mm_dec n x0 p0) (@nil (mm_instr n)))) (@pair nat (list (mm_instr n)) i (@cons (mm_instr n) (@mm_dec n x p) ll))) (or (@eq eill_cmd A (in_ll_cmd_fork (ry x0) (q p0) (q j))) (@eq eill_cmd A (in_ll_cmd_dec (rx x0) (q (Init.Nat.add (S O) j)) (q j)))))))) *)
    right; exists i, x, p; split; auto.
(* Goal: or (@ex nat (fun j : nat => @ex (pos n) (fun x0 : pos n => and (@subcode (mm_instr n) (@pair nat (list (mm_instr n)) j (@cons (mm_instr n) (@mm_inc n x0) (@nil (mm_instr n)))) (@pair nat (list (mm_instr n)) i (@cons (mm_instr n) (@mm_dec n x p) ll))) (@eq eill_cmd A (in_ll_cmd_inc (rx x0) (q (Init.Nat.add (S O) j)) (q j)))))) (@ex nat (fun j : nat => @ex (pos n) (fun x0 : pos n => @ex nat (fun p0 : nat => and (@subcode (mm_instr n) (@pair nat (list (mm_instr n)) j (@cons (mm_instr n) (@mm_dec n x0 p0) (@nil (mm_instr n)))) (@pair nat (list (mm_instr n)) i (@cons (mm_instr n) (@mm_dec n x p) ll))) (or (@eq eill_cmd A (in_ll_cmd_fork (ry x0) (q p0) (q j))) (@eq eill_cmd A (in_ll_cmd_dec (rx x0) (q (Init.Nat.add (S O) j)) (q j)))))))) *)
    destruct HA as [ HA | HA ].
(* Goal: or (@ex nat (fun j : nat => @ex (pos n) (fun x0 : pos n => and (@subcode (mm_instr n) (@pair nat (list (mm_instr n)) j (@cons (mm_instr n) (@mm_inc n x0) (@nil (mm_instr n)))) (@pair nat (list (mm_instr n)) i (@cons (mm_instr n) (@mm_dec n x p) ll))) (@eq eill_cmd A (in_ll_cmd_inc (rx x0) (q (Init.Nat.add (S O) j)) (q j)))))) (@ex nat (fun j : nat => @ex (pos n) (fun x0 : pos n => @ex nat (fun p0 : nat => and (@subcode (mm_instr n) (@pair nat (list (mm_instr n)) j (@cons (mm_instr n) (@mm_dec n x0 p0) (@nil (mm_instr n)))) (@pair nat (list (mm_instr n)) i (@cons (mm_instr n) (@mm_dec n x p) ll))) (or (@eq eill_cmd A (in_ll_cmd_fork (ry x0) (q p0) (q j))) (@eq eill_cmd A (in_ll_cmd_dec (rx x0) (q (Init.Nat.add (S O) j)) (q j)))))))) *)
(* Goal: or (@ex nat (fun j : nat => @ex (pos n) (fun x0 : pos n => and (@subcode (mm_instr n) (@pair nat (list (mm_instr n)) j (@cons (mm_instr n) (@mm_inc n x0) (@nil (mm_instr n)))) (@pair nat (list (mm_instr n)) i (@cons (mm_instr n) (@mm_dec n x p) ll))) (@eq eill_cmd A (in_ll_cmd_inc (rx x0) (q (Init.Nat.add (S O) j)) (q j)))))) (@ex nat (fun j : nat => @ex (pos n) (fun x0 : pos n => @ex nat (fun p0 : nat => and (@subcode (mm_instr n) (@pair nat (list (mm_instr n)) j (@cons (mm_instr n) (@mm_dec n x0 p0) (@nil (mm_instr n)))) (@pair nat (list (mm_instr n)) i (@cons (mm_instr n) (@mm_dec n x p) ll))) (or (@eq eill_cmd A (in_ll_cmd_fork (ry x0) (q p0) (q j))) (@eq eill_cmd A (in_ll_cmd_dec (rx x0) (q (Init.Nat.add (S O) j)) (q j)))))))) *)
    right; exists i, x, p; split; auto.
(* Goal: or (@ex nat (fun j : nat => @ex (pos n) (fun x0 : pos n => and (@subcode (mm_instr n) (@pair nat (list (mm_instr n)) j (@cons (mm_instr n) (@mm_inc n x0) (@nil (mm_instr n)))) (@pair nat (list (mm_instr n)) i (@cons (mm_instr n) (@mm_dec n x p) ll))) (@eq eill_cmd A (in_ll_cmd_inc (rx x0) (q (Init.Nat.add (S O) j)) (q j)))))) (@ex nat (fun j : nat => @ex (pos n) (fun x0 : pos n => @ex nat (fun p0 : nat => and (@subcode (mm_instr n) (@pair nat (list (mm_instr n)) j (@cons (mm_instr n) (@mm_dec n x0 p0) (@nil (mm_instr n)))) (@pair nat (list (mm_instr n)) i (@cons (mm_instr n) (@mm_dec n x p) ll))) (or (@eq eill_cmd A (in_ll_cmd_fork (ry x0) (q p0) (q j))) (@eq eill_cmd A (in_ll_cmd_dec (rx x0) (q (Init.Nat.add (S O) j)) (q j)))))))) *)
    apply IHll in HA.
(* Goal: or (@ex nat (fun j : nat => @ex (pos n) (fun x0 : pos n => and (@subcode (mm_instr n) (@pair nat (list (mm_instr n)) j (@cons (mm_instr n) (@mm_inc n x0) (@nil (mm_instr n)))) (@pair nat (list (mm_instr n)) i (@cons (mm_instr n) (@mm_dec n x p) ll))) (@eq eill_cmd A (in_ll_cmd_inc (rx x0) (q (Init.Nat.add (S O) j)) (q j)))))) (@ex nat (fun j : nat => @ex (pos n) (fun x0 : pos n => @ex nat (fun p0 : nat => and (@subcode (mm_instr n) (@pair nat (list (mm_instr n)) j (@cons (mm_instr n) (@mm_dec n x0 p0) (@nil (mm_instr n)))) (@pair nat (list (mm_instr n)) i (@cons (mm_instr n) (@mm_dec n x p) ll))) (or (@eq eill_cmd A (in_ll_cmd_fork (ry x0) (q p0) (q j))) (@eq eill_cmd A (in_ll_cmd_dec (rx x0) (q (Init.Nat.add (S O) j)) (q j)))))))) *)
    destruct HA as [ (j & x' & H1 & H2) | (j & x' & p' & H1 & H2) ].
(* Goal: or (@ex nat (fun j : nat => @ex (pos n) (fun x0 : pos n => and (@subcode (mm_instr n) (@pair nat (list (mm_instr n)) j (@cons (mm_instr n) (@mm_inc n x0) (@nil (mm_instr n)))) (@pair nat (list (mm_instr n)) i (@cons (mm_instr n) (@mm_dec n x p) ll))) (@eq eill_cmd A (in_ll_cmd_inc (rx x0) (q (Init.Nat.add (S O) j)) (q j)))))) (@ex nat (fun j : nat => @ex (pos n) (fun x0 : pos n => @ex nat (fun p0 : nat => and (@subcode (mm_instr n) (@pair nat (list (mm_instr n)) j (@cons (mm_instr n) (@mm_dec n x0 p0) (@nil (mm_instr n)))) (@pair nat (list (mm_instr n)) i (@cons (mm_instr n) (@mm_dec n x p) ll))) (or (@eq eill_cmd A (in_ll_cmd_fork (ry x0) (q p0) (q j))) (@eq eill_cmd A (in_ll_cmd_dec (rx x0) (q (Init.Nat.add (S O) j)) (q j)))))))) *)
(* Goal: or (@ex nat (fun j : nat => @ex (pos n) (fun x0 : pos n => and (@subcode (mm_instr n) (@pair nat (list (mm_instr n)) j (@cons (mm_instr n) (@mm_inc n x0) (@nil (mm_instr n)))) (@pair nat (list (mm_instr n)) i (@cons (mm_instr n) (@mm_dec n x p) ll))) (@eq eill_cmd A (in_ll_cmd_inc (rx x0) (q (Init.Nat.add (S O) j)) (q j)))))) (@ex nat (fun j : nat => @ex (pos n) (fun x0 : pos n => @ex nat (fun p0 : nat => and (@subcode (mm_instr n) (@pair nat (list (mm_instr n)) j (@cons (mm_instr n) (@mm_dec n x0 p0) (@nil (mm_instr n)))) (@pair nat (list (mm_instr n)) i (@cons (mm_instr n) (@mm_dec n x p) ll))) (or (@eq eill_cmd A (in_ll_cmd_fork (ry x0) (q p0) (q j))) (@eq eill_cmd A (in_ll_cmd_dec (rx x0) (q (Init.Nat.add (S O) j)) (q j)))))))) *)
    left; exists j, x'; split; auto.
(* Goal: @subcode (mm_instr n) (@pair nat (list (mm_instr n)) j (@cons (mm_instr n) (@mm_dec n x' p') (@nil (mm_instr n)))) (@pair nat (list (mm_instr n)) i (@cons (mm_instr n) (@mm_dec n x p) ll)) *)
    apply subcode_trans with (1 := H1); subcode_tac; solve list eq.
(* Goal: or (@ex nat (fun j : nat => @ex (pos n) (fun x0 : pos n => and (@subcode (mm_instr n) (@pair nat (list (mm_instr n)) j (@cons (mm_instr n) (@mm_inc n x0) (@nil (mm_instr n)))) (@pair nat (list (mm_instr n)) i (@cons (mm_instr n) (@mm_dec n x p) ll))) (@eq eill_cmd A (in_ll_cmd_inc (rx x0) (q (Init.Nat.add (S O) j)) (q j)))))) (@ex nat (fun j : nat => @ex (pos n) (fun x0 : pos n => @ex nat (fun p0 : nat => and (@subcode (mm_instr n) (@pair nat (list (mm_instr n)) j (@cons (mm_instr n) (@mm_dec n x0 p0) (@nil (mm_instr n)))) (@pair nat (list (mm_instr n)) i (@cons (mm_instr n) (@mm_dec n x p) ll))) (or (@eq eill_cmd A (in_ll_cmd_fork (ry x0) (q p0) (q j))) (@eq eill_cmd A (in_ll_cmd_dec (rx x0) (q (Init.Nat.add (S O) j)) (q j)))))))) *)
    right; exists j, x', p'; split; auto.
(* Goal: @subcode (mm_instr n) (@pair nat (list (mm_instr n)) j (@cons (mm_instr n) (@mm_dec n x' p') (@nil (mm_instr n)))) (@pair nat (list (mm_instr n)) i (@cons (mm_instr n) (@mm_dec n x p) ll)) *)
    apply subcode_trans with (1 := H1); subcode_tac; solve list eq.
  Qed.

  (* k is a position outside the program were execution has to stop *)
   
  Variable (P : nat*(list (mm_instr n))) (k : nat) (Hk : out_code k P).

  (* This encodes P into EILL commands 
  
     (q k)  terminates on an zero vector
     (ry j) terminates on a vector vec there is no (rx j)
     
  *)
                  
  Definition Sig0 := LL_INC (q k) (q k) (q k)
                  :: map (fun c => LL_DEC (rx (fst c)) (ry (snd c)) (ry (snd c))) (pos_not_diag n)
                  ++ map (fun j => LL_INC (ry j) (ry j) (ry j)) (pos_list n).

  Definition SigI := match P with (i,l) => mm_linstr_enc i l end.

  Definition Sig := Sig0 ++ SigI.

  Notation "P // s -[ k ]-> t" := (sss_steps (@mm_sss _) P k s t).
  Notation "P // s ->> t" := (sss_compute (@mm_sss _) P s t).

  (* We define the semantics as in the paper ToCL 2013 (DLW & Galmiche) *)

  Local Definition s (x : ll_vars) (v : vec nat n) : Prop.
  Proof.
    refine (match le_lt_dec n x with
                 | left H1  => match le_lt_dec (2*n) x with
                     | left _   => P // (x-2*n,v) ->> (k,vec_zero)
                     | right H2 => vec_pos v (@nat2pos n (x-n) _) = 0
                   end
                 | right H1 => v = vec_one (@nat2pos n x H1)
(* Goal: @eq nat (@vec_pos nat n v p) O *)
(* Goal: G_eill Sig0 (@app nat (@vec_map_list nat n w rx) Ga) (ry p) *)
               end); omega.
  Defined.

  (* We check the required properties *)

  Let H_s_q : forall i v, s (q i) v <-> P // (i,v) ->> (k,vec_zero).
  Proof.
(* Goal: forall (i : nat) (v : vec nat n), iff (s (q i) v) (@sss_compute (mm_instr n) (vec nat n) (@mm_sss n) P (@pair nat (vec nat n) i v) (@pair nat (vec nat n) k (@vec_zero n))) *)
    intros i v; unfold q, s.
(* Goal: iff match le_lt_dec n (Init.Nat.add (Init.Nat.mul (S (S O)) n) i) with | left H1 => match le_lt_dec (Init.Nat.mul (S (S O)) n) (Init.Nat.add (Init.Nat.mul (S (S O)) n) i) with | left l => @sss_compute (mm_instr n) (vec nat n) (@mm_sss n) P (@pair nat (vec nat n) (Init.Nat.sub (Init.Nat.add (Init.Nat.mul (S (S O)) n) i) (Init.Nat.mul (S (S O)) n)) v) (@pair nat (vec nat n) k (@vec_zero n)) | right H2 => @eq nat (@vec_pos nat n v (@nat2pos n (Init.Nat.sub (Init.Nat.add (Init.Nat.mul (S (S O)) n) i) n) (Decidable.dec_not_not (lt (Init.Nat.sub (Init.Nat.add (Init.Nat.mul (S (S O)) n) i) n) n) (dec_lt (Init.Nat.sub (Init.Nat.add (Init.Nat.mul (S (S O)) n) i) n) n) (fun H : not (lt (Init.Nat.sub (Init.Nat.add (Init.Nat.mul (S (S O)) n) i) n) n) => @eq_ind_r Z (Z.mul (Z.of_nat (S (S O))) (Z.of_nat n)) (fun x : Z => forall _ : Z.lt (Z.of_nat (Init.Nat.add (Init.Nat.mul (S (S O)) n) i)) x, False) (fun H3 : Z.lt (Z.of_nat (Init.Nat.add (Init.Nat.mul (S (S O)) n) i)) (Z.mul (Zpos (xO xH)) (Z.of_nat n)) => @sumbool_ind (le n (Init.Nat.add (Init.Nat.mul (S (S O)) n) i)) (gt n (Init.Nat.add (Init.Nat.mul (S (S O)) n) i)) (fun _ : sumbool (le n (Init.Nat.add (Init.Nat.mul (S (S O)) n) i)) (gt n (Init.Nat.add (Init.Nat.mul (S (S O)) n) i)) => forall _ : Z.ge (Z.of_nat (Init.Nat.sub (Init.Nat.add (Init.Nat.mul (S (S O)) n) i) n)) (Z.of_nat n), False) (fun Omega0 : le n (Init.Nat.add (Init.Nat.mul (S (S O)) n) i) => @eq_ind_r Z (Z.sub (Z.of_nat (Init.Nat.add (Init.Nat.mul (S (S O)) n) i)) (Z.of_nat n)) (fun x : Z => forall _ : Z.ge x (Z.of_nat n), False) (fun H0 : Z.ge (Z.sub (Z.of_nat (Init.Nat.add (Init.Nat.mul (S (S O)) n) i)) (Z.of_nat n)) (Z.of_nat n) => @ex_ind Z (fun y : Z => and (@eq Z (Z.of_nat (Init.Nat.add (Init.Nat.mul (S (S O)) n) i)) y) (Z.le Z0 (Z.add (Z.mul y (Zpos xH)) Z0))) False (fun (Zvar0 : Z) (Omega8 : and (@eq Z (Z.of_nat (Init.Nat.add (Init.Nat.mul (S (S O)) n) i)) Zvar0) (Z.le Z0 (Z.add (Z.mul Zvar0 (Zpos xH)) Z0))) => @and_ind (@eq Z (Z.of_nat (Init.Nat.add (Init.Nat.mul (S (S O)) n) i)) Zvar0) (Z.le Z0 (Z.add (Z.mul Zvar0 (Zpos xH)) Z0)) False (fun (Omega1 : @eq Z (Z.of_nat (Init.Nat.add (Init.Nat.mul (S (S O)) n) i)) Zvar0) (_ : Z.le Z0 (Z.add (Z.mul Zvar0 (Zpos xH)) Z0)) => @ex_ind Z (fun y : Z => and (@eq Z (Z.of_nat n) y) (Z.le Z0 (Z.add (Z.mul y (Zpos xH)) Z0))) False (fun (Zvar1 : Z) (Omega7 : and (@eq Z (Z.of_nat n) Zvar1) (Z.le Z0 (Z.add (Z.mul Zvar1 (Zpos xH)) Z0))) => @and_ind (@eq Z (Z.of_nat n) Zvar1) (Z.le Z0 (Z.add (Z.mul Zvar1 (Zpos xH)) Z0)) False (fun (Omega2 : @eq Z (Z.of_nat n) Zvar1) (_ : Z.le Z0 (Z.add (Z.mul Zvar1 (Zpos xH)) Z0)) => @eq_ind_r Z Zvar1 (fun x : Z => forall _ : Z.le Z0 (Z.add (Z.add (Z.mul (Zpos (xO xH)) x) (Zneg xH)) (Z.opp (Z.of_nat (Init.Nat.add (Init.Nat.mul (S (S O)) n) i)))), False) (fast_Zmult_comm (Zpos (xO xH)) Zvar1 (fun x : Z => forall _ : Z.le Z0 (Z.add (Z.add x (Zneg xH)) (Z.opp (Z.of_nat (Init.Nat.add (Init.Nat.mul (S (S O)) n) i)))), False) (@eq_ind_r Z Zvar0 (fun x : Z => forall _ : Z.le Z0 (Z.add (Z.add (Z.mul Zvar1 (Zpos (xO xH))) (Zneg xH)) (Z.opp x)), False) (fast_Zopp_eq_mult_neg_1 Zvar0 (fun x : Z => forall _ : Z.le Z0 (Z.add (Z.add (Z.mul Zvar1 (Zpos (xO xH))) (Zneg xH)) x), False) (fast_Zplus_comm (Z.add (Z.mul Zvar1 (Zpos (xO xH))) (Zneg xH)) (Z.mul Zvar0 (Zneg xH)) (fun x : Z => forall _ : Z.le Z0 x, False) (fun Omega5 : Z.le Z0 (Z.add (Z.mul Zvar0 (Zneg xH)) (Z.add (Z.mul Zvar1 (Zpos (xO xH))) (Zneg xH))) => @eq_ind_r Z Zvar0 (fun x : Z => forall _ : Z.le Z0 (Z.add (Z.add x (Z.opp (Z.of_nat n))) (Z.opp (Z.of_nat n))), False) (@eq_ind_r Z Zvar1 (fun x : Z => forall _ : Z.le Z0 (Z.add (Z.add Zvar0 (Z.opp x)) (Z.opp (Z.of_nat n))), False) (fast_Zopp_eq_mult_neg_1 Zvar1 (fun x : Z => forall _ : Z.le Z0 (Z.add (Z.add Zvar0 x) (Z.opp (Z.of_nat n))), False) (@eq_ind_r Z Zvar1 (fun x : Z => forall _ : Z.le Z0 (Z.add (Z.add Zvar0 (Z.mul Zvar1 (Zneg xH))) (Z.opp x)), False) (fast_Zopp_eq_mult_neg_1 Zvar1 (fun x : Z => forall _ : Z.le Z0 (Z.add (Z.add Zvar0 (Z.mul Zvar1 (Zneg xH))) x), False) (fast_Zplus_assoc_reverse Zvar0 (Z.mul Zvar1 (Zneg xH)) (Z.mul Zvar1 (Zneg xH)) (fun x : Z => forall _ : Z.le Z0 x, False) (fast_Zred_factor0 Zvar0 (fun x : Z => forall _ : Z.le Z0 (Z.add x (Z.add (Z.mul Zvar1 (Zneg xH)) (Z.mul Zvar1 (Zneg xH)))), False) (fast_Zred_factor4 Zvar1 (Zneg xH) (Zneg xH) (fun x : Z => forall _ : Z.le Z0 (Z.add (Z.mul Zvar0 (Zpos xH)) x), False) (fast_Zred_factor6 (Z.mul Zvar1 (Zneg (xO xH))) (fun x : Z => forall _ : Z.le Z0 (Z.add (Z.mul Zvar0 (Zpos xH)) x), False) (fun Omega3 : Z.le Z0 (Z.add (Z.mul Zvar0 (Zpos xH)) (Z.add (Z.mul Zvar1 (Zneg (xO xH))) Z0)) => fast_OMEGA13 Zvar0 (Z.add (Z.mul Zvar1 (Zneg (xO xH))) Z0) (Z.add (Z.mul Zvar1 (Zpos (xO xH))) (Zneg xH)) xH (fun x : Z => forall _ : Z.le Z0 x, False) (fast_OMEGA14 Zvar1 Z0 (Zneg xH) (xO xH) (fun x : Z => forall _ : Z.le Z0 x, False) (fun H4 : not (@eq comparison Gt Gt) => False_ind False (H4 (@eq_refl comparison Gt)))) (OMEGA2 (Z.add (Z.mul Zvar0 (Zpos xH)) (Z.add (Z.mul Zvar1 (Zneg (xO xH))) Z0)) (Z.add (Z.mul Zvar0 (Zneg xH)) (Z.add (Z.mul Zvar1 (Zpos (xO xH))) (Zneg xH))) Omega3 Omega5))))))) (Z.of_nat n) Omega2)) (Z.of_nat n) Omega2) (Z.of_nat (Init.Nat.add (Init.Nat.mul (S (S O)) n) i)) Omega1 (Zge_left (Z.sub (Z.of_nat (Init.Nat.add (Init.Nat.mul (S (S O)) n) i)) (Z.of_nat n)) (Z.of_nat n) H0)))) (Z.of_nat (Init.Nat.add (Init.Nat.mul (S (S O)) n) i)) Omega1)) (Z.of_nat n) Omega2 (Zlt_left (Z.of_nat (Init.Nat.add (Init.Nat.mul (S (S O)) n) i)) (Z.mul (Zpos (xO xH)) (Z.of_nat n)) H3)) Omega7) (intro_Z n)) Omega8) (intro_Z (Init.Nat.add (Init.Nat.mul (S (S O)) n) i))) (Z.of_nat (Init.Nat.sub (Init.Nat.add (Init.Nat.mul (S (S O)) n) i) n)) (Nat2Z.inj_sub (Init.Nat.add (Init.Nat.mul (S (S O)) n) i) n Omega0)) (fun Omega0 : gt n (Init.Nat.add (Init.Nat.mul (S (S O)) n) i) => @eq_ind_r Z Z0 (fun x : Z => forall _ : Z.ge x (Z.of_nat n), False) (fun _ : Z.ge Z0 (Z.of_nat n) => @ex_ind Z (fun y : Z => and (@eq Z (Z.of_nat n) y) (Z.le Z0 (Z.add (Z.mul y (Zpos xH)) Z0))) False (fun (Zvar2 : Z) (Omega16 : and (@eq Z (Z.of_nat n) Zvar2) (Z.le Z0 (Z.add (Z.mul Zvar2 (Zpos xH)) Z0))) => @and_ind (@eq Z (Z.of_nat n) Zvar2) (Z.le Z0 (Z.add (Z.mul Zvar2 (Zpos xH)) Z0)) False (fun (Omega9 : @eq Z (Z.of_nat n) Zvar2) (_ : Z.le Z0 (Z.add (Z.mul Zvar2 (Zpos xH)) Z0)) => @ex_ind Z (fun y : Z => and (@eq Z (Z.of_nat (Init.Nat.add (Init.Nat.mul (S (S O)) n) i)) y) (Z.le Z0 (Z.add (Z.mul y (Zpos xH)) Z0))) False (fun (Zvar3 : Z) (Omega15 : and (@eq Z (Z.of_nat (Init.Nat.add (Init.Nat.mul (S (S O)) n) i)) Zvar3) (Z.le Z0 (Z.add (Z.mul Zvar3 (Zpos xH)) Z0))) => @and_ind (@eq Z (Z.of_nat (Init.Nat.add (Init.Nat.mul (S (S O)) n) i)) Zvar3) (Z.le Z0 (Z.add (Z.mul Zvar3 (Zpos xH)) Z0)) False (fun (Omega11 : @eq Z (Z.of_nat (Init.Nat.add (Init.Nat.mul (S (S O)) n) i)) Zvar3) (_ : Z.le Z0 (Z.add (Z.mul Zvar3 (Zpos xH)) Z0)) => @eq_ind_r Z Zvar3 (fun x : Z => forall _ : Z.le Z0 (Z.add x (Z.opp (Z.of_nat n))), False) (@eq_ind_r Z Zvar2 (fun x : Z => forall _ : Z.le Z0 (Z.add Zvar3 (Z.opp x)), False) (fast_Zopp_eq_mult_neg_1 Zvar2 (fun x : Z => forall _ : Z.le Z0 (Z.add Zvar3 x), False) (fast_Zred_factor0 Zvar3 (fun x : Z => forall _ : Z.le Z0 (Z.add x (Z.mul Zvar2 (Zneg xH))), False) (fast_Zred_factor6 (Z.mul Zvar2 (Zneg xH)) (fun x : Z => forall _ : Z.le Z0 (Z.add (Z.mul Zvar3 (Zpos xH)) x), False) (fun Omega14 : Z.le Z0 (Z.add (Z.mul Zvar3 (Zpos xH)) (Z.add (Z.mul Zvar2 (Zneg xH)) Z0)) => @eq_ind_r Z Zvar2 (fun x : Z => forall _ : Z.le Z0 (Z.add (Z.add x (Zneg xH)) (Z.opp (Z.of_nat (Init.Nat.add (Init.Nat.mul (S (S O)) n) i)))), False) (@eq_ind_r Z Zvar3 (fun x : Z => forall _ : Z.le Z0 (Z.add (Z.add Zvar2 (Zneg xH)) (Z.opp x)), False) (fast_Zopp_eq_mult_neg_1 Zvar3 (fun x : Z => forall _ : Z.le Z0 (Z.add (Z.add Zvar2 (Zneg xH)) x), False) (fast_Zplus_comm (Z.add Zvar2 (Zneg xH)) (Z.mul Zvar3 (Zneg xH)) (fun x : Z => forall _ : Z.le Z0 x, False) (fast_Zred_factor0 Zvar2 (fun x : Z => forall _ : Z.le Z0 (Z.add (Z.mul Zvar3 (Zneg xH)) (Z.add x (Zneg xH))), False) (fun Omega12 : Z.le Z0 (Z.add (Z.mul Zvar3 (Zneg xH)) (Z.add (Z.mul Zvar2 (Zpos xH)) (Zneg xH))) => fast_OMEGA13 Zvar3 (Z.add (Z.mul Zvar2 (Zneg xH)) Z0) (Z.add (Z.mul Zvar2 (Zpos xH)) (Zneg xH)) xH (fun x : Z => forall _ : Z.le Z0 x, False) (fast_OMEGA14 Zvar2 Z0 (Zneg xH) xH (fun x : Z => forall _ : Z.le Z0 x, False) (fun H4 : not (@eq comparison Gt Gt) => False_ind False (H4 (@eq_refl comparison Gt)))) (OMEGA2 (Z.add (Z.mul Zvar3 (Zpos xH)) (Z.add (Z.mul Zvar2 (Zneg xH)) Z0)) (Z.add (Z.mul Zvar3 (Zneg xH)) (Z.add (Z.mul Zvar2 (Zpos xH)) (Zneg xH))) Omega14 Omega12))))) (Z.of_nat (Init.Nat.add (Init.Nat.mul (S (S O)) n) i)) Omega11) (Z.of_nat n) Omega9 (Zgt_left (Z.of_nat n) (Z.of_nat (Init.Nat.add (Init.Nat.mul (S (S O)) n) i)) (inj_gt n (Init.Nat.add (Init.Nat.mul (S (S O)) n) i) Omega0)))))) (Z.of_nat n) Omega9) (Z.of_nat (Init.Nat.add (Init.Nat.mul (S (S O)) n) i)) Omega11 (Zle_left (Z.of_nat n) (Z.of_nat (Init.Nat.add (Init.Nat.mul (S (S O)) n) i)) (inj_le n (Init.Nat.add (Init.Nat.mul (S (S O)) n) i) H1))) Omega15) (intro_Z (Init.Nat.add (Init.Nat.mul (S (S O)) n) i))) Omega16) (intro_Z n)) (Z.of_nat (Init.Nat.sub (Init.Nat.add (Init.Nat.mul (S (S O)) n) i) n)) (inj_minus2 (Init.Nat.add (Init.Nat.mul (S (S O)) n) i) n Omega0)) (le_gt_dec n (Init.Nat.add (Init.Nat.mul (S (S O)) n) i)) (inj_ge (Init.Nat.sub (Init.Nat.add (Init.Nat.mul (S (S O)) n) i) n) n (not_lt (Init.Nat.sub (Init.Nat.add (Init.Nat.mul (S (S O)) n) i) n) n H))) (Z.of_nat (Init.Nat.mul (S (S O)) n)) (Nat2Z.inj_mul (S (S O)) n) (inj_lt (Init.Nat.add (Init.Nat.mul (S (S O)) n) i) (Init.Nat.mul (S (S O)) n) H2))))) O end | right H1 => @eq (vec nat n) v (@vec_one n (@nat2pos n (Init.Nat.add (Init.Nat.mul (S (S O)) n) i) H1)) end (@sss_compute (mm_instr n) (vec nat n) (@mm_sss n) P (@pair nat (vec nat n) i v) (@pair nat (vec nat n) k (@vec_zero n))) *)
    destruct (le_lt_dec n (2*n+i)); [ | omega ].
(* Goal: iff match le_lt_dec (Init.Nat.mul (S (S O)) n) (Init.Nat.add (Init.Nat.mul (S (S O)) n) i) with | left l => @sss_compute (mm_instr n) (vec nat n) (@mm_sss n) P (@pair nat (vec nat n) (Init.Nat.sub (Init.Nat.add (Init.Nat.mul (S (S O)) n) i) (Init.Nat.mul (S (S O)) n)) v) (@pair nat (vec nat n) k (@vec_zero n)) | right H2 => @eq nat (@vec_pos nat n v (@nat2pos n (Init.Nat.sub (Init.Nat.add (Init.Nat.mul (S (S O)) n) i) n) (Decidable.dec_not_not (lt (Init.Nat.sub (Init.Nat.add (Init.Nat.mul (S (S O)) n) i) n) n) (dec_lt (Init.Nat.sub (Init.Nat.add (Init.Nat.mul (S (S O)) n) i) n) n) (fun H : not (lt (Init.Nat.sub (Init.Nat.add (Init.Nat.mul (S (S O)) n) i) n) n) => @eq_ind_r Z (Z.mul (Z.of_nat (S (S O))) (Z.of_nat n)) (fun x : Z => forall _ : Z.lt (Z.of_nat (Init.Nat.add (Init.Nat.mul (S (S O)) n) i)) x, False) (fun H3 : Z.lt (Z.of_nat (Init.Nat.add (Init.Nat.mul (S (S O)) n) i)) (Z.mul (Zpos (xO xH)) (Z.of_nat n)) => @sumbool_ind (le n (Init.Nat.add (Init.Nat.mul (S (S O)) n) i)) (gt n (Init.Nat.add (Init.Nat.mul (S (S O)) n) i)) (fun _ : sumbool (le n (Init.Nat.add (Init.Nat.mul (S (S O)) n) i)) (gt n (Init.Nat.add (Init.Nat.mul (S (S O)) n) i)) => forall _ : Z.ge (Z.of_nat (Init.Nat.sub (Init.Nat.add (Init.Nat.mul (S (S O)) n) i) n)) (Z.of_nat n), False) (fun Omega0 : le n (Init.Nat.add (Init.Nat.mul (S (S O)) n) i) => @eq_ind_r Z (Z.sub (Z.of_nat (Init.Nat.add (Init.Nat.mul (S (S O)) n) i)) (Z.of_nat n)) (fun x : Z => forall _ : Z.ge x (Z.of_nat n), False) (fun H0 : Z.ge (Z.sub (Z.of_nat (Init.Nat.add (Init.Nat.mul (S (S O)) n) i)) (Z.of_nat n)) (Z.of_nat n) => @ex_ind Z (fun y : Z => and (@eq Z (Z.of_nat (Init.Nat.add (Init.Nat.mul (S (S O)) n) i)) y) (Z.le Z0 (Z.add (Z.mul y (Zpos xH)) Z0))) False (fun (Zvar0 : Z) (Omega8 : and (@eq Z (Z.of_nat (Init.Nat.add (Init.Nat.mul (S (S O)) n) i)) Zvar0) (Z.le Z0 (Z.add (Z.mul Zvar0 (Zpos xH)) Z0))) => @and_ind (@eq Z (Z.of_nat (Init.Nat.add (Init.Nat.mul (S (S O)) n) i)) Zvar0) (Z.le Z0 (Z.add (Z.mul Zvar0 (Zpos xH)) Z0)) False (fun (Omega1 : @eq Z (Z.of_nat (Init.Nat.add (Init.Nat.mul (S (S O)) n) i)) Zvar0) (_ : Z.le Z0 (Z.add (Z.mul Zvar0 (Zpos xH)) Z0)) => @ex_ind Z (fun y : Z => and (@eq Z (Z.of_nat n) y) (Z.le Z0 (Z.add (Z.mul y (Zpos xH)) Z0))) False (fun (Zvar1 : Z) (Omega7 : and (@eq Z (Z.of_nat n) Zvar1) (Z.le Z0 (Z.add (Z.mul Zvar1 (Zpos xH)) Z0))) => @and_ind (@eq Z (Z.of_nat n) Zvar1) (Z.le Z0 (Z.add (Z.mul Zvar1 (Zpos xH)) Z0)) False (fun (Omega2 : @eq Z (Z.of_nat n) Zvar1) (_ : Z.le Z0 (Z.add (Z.mul Zvar1 (Zpos xH)) Z0)) => @eq_ind_r Z Zvar1 (fun x : Z => forall _ : Z.le Z0 (Z.add (Z.add (Z.mul (Zpos (xO xH)) x) (Zneg xH)) (Z.opp (Z.of_nat (Init.Nat.add (Init.Nat.mul (S (S O)) n) i)))), False) (fast_Zmult_comm (Zpos (xO xH)) Zvar1 (fun x : Z => forall _ : Z.le Z0 (Z.add (Z.add x (Zneg xH)) (Z.opp (Z.of_nat (Init.Nat.add (Init.Nat.mul (S (S O)) n) i)))), False) (@eq_ind_r Z Zvar0 (fun x : Z => forall _ : Z.le Z0 (Z.add (Z.add (Z.mul Zvar1 (Zpos (xO xH))) (Zneg xH)) (Z.opp x)), False) (fast_Zopp_eq_mult_neg_1 Zvar0 (fun x : Z => forall _ : Z.le Z0 (Z.add (Z.add (Z.mul Zvar1 (Zpos (xO xH))) (Zneg xH)) x), False) (fast_Zplus_comm (Z.add (Z.mul Zvar1 (Zpos (xO xH))) (Zneg xH)) (Z.mul Zvar0 (Zneg xH)) (fun x : Z => forall _ : Z.le Z0 x, False) (fun Omega5 : Z.le Z0 (Z.add (Z.mul Zvar0 (Zneg xH)) (Z.add (Z.mul Zvar1 (Zpos (xO xH))) (Zneg xH))) => @eq_ind_r Z Zvar0 (fun x : Z => forall _ : Z.le Z0 (Z.add (Z.add x (Z.opp (Z.of_nat n))) (Z.opp (Z.of_nat n))), False) (@eq_ind_r Z Zvar1 (fun x : Z => forall _ : Z.le Z0 (Z.add (Z.add Zvar0 (Z.opp x)) (Z.opp (Z.of_nat n))), False) (fast_Zopp_eq_mult_neg_1 Zvar1 (fun x : Z => forall _ : Z.le Z0 (Z.add (Z.add Zvar0 x) (Z.opp (Z.of_nat n))), False) (@eq_ind_r Z Zvar1 (fun x : Z => forall _ : Z.le Z0 (Z.add (Z.add Zvar0 (Z.mul Zvar1 (Zneg xH))) (Z.opp x)), False) (fast_Zopp_eq_mult_neg_1 Zvar1 (fun x : Z => forall _ : Z.le Z0 (Z.add (Z.add Zvar0 (Z.mul Zvar1 (Zneg xH))) x), False) (fast_Zplus_assoc_reverse Zvar0 (Z.mul Zvar1 (Zneg xH)) (Z.mul Zvar1 (Zneg xH)) (fun x : Z => forall _ : Z.le Z0 x, False) (fast_Zred_factor0 Zvar0 (fun x : Z => forall _ : Z.le Z0 (Z.add x (Z.add (Z.mul Zvar1 (Zneg xH)) (Z.mul Zvar1 (Zneg xH)))), False) (fast_Zred_factor4 Zvar1 (Zneg xH) (Zneg xH) (fun x : Z => forall _ : Z.le Z0 (Z.add (Z.mul Zvar0 (Zpos xH)) x), False) (fast_Zred_factor6 (Z.mul Zvar1 (Zneg (xO xH))) (fun x : Z => forall _ : Z.le Z0 (Z.add (Z.mul Zvar0 (Zpos xH)) x), False) (fun Omega3 : Z.le Z0 (Z.add (Z.mul Zvar0 (Zpos xH)) (Z.add (Z.mul Zvar1 (Zneg (xO xH))) Z0)) => fast_OMEGA13 Zvar0 (Z.add (Z.mul Zvar1 (Zneg (xO xH))) Z0) (Z.add (Z.mul Zvar1 (Zpos (xO xH))) (Zneg xH)) xH (fun x : Z => forall _ : Z.le Z0 x, False) (fast_OMEGA14 Zvar1 Z0 (Zneg xH) (xO xH) (fun x : Z => forall _ : Z.le Z0 x, False) (fun H1 : not (@eq comparison Gt Gt) => False_ind False (H1 (@eq_refl comparison Gt)))) (OMEGA2 (Z.add (Z.mul Zvar0 (Zpos xH)) (Z.add (Z.mul Zvar1 (Zneg (xO xH))) Z0)) (Z.add (Z.mul Zvar0 (Zneg xH)) (Z.add (Z.mul Zvar1 (Zpos (xO xH))) (Zneg xH))) Omega3 Omega5))))))) (Z.of_nat n) Omega2)) (Z.of_nat n) Omega2) (Z.of_nat (Init.Nat.add (Init.Nat.mul (S (S O)) n) i)) Omega1 (Zge_left (Z.sub (Z.of_nat (Init.Nat.add (Init.Nat.mul (S (S O)) n) i)) (Z.of_nat n)) (Z.of_nat n) H0)))) (Z.of_nat (Init.Nat.add (Init.Nat.mul (S (S O)) n) i)) Omega1)) (Z.of_nat n) Omega2 (Zlt_left (Z.of_nat (Init.Nat.add (Init.Nat.mul (S (S O)) n) i)) (Z.mul (Zpos (xO xH)) (Z.of_nat n)) H3)) Omega7) (intro_Z n)) Omega8) (intro_Z (Init.Nat.add (Init.Nat.mul (S (S O)) n) i))) (Z.of_nat (Init.Nat.sub (Init.Nat.add (Init.Nat.mul (S (S O)) n) i) n)) (Nat2Z.inj_sub (Init.Nat.add (Init.Nat.mul (S (S O)) n) i) n Omega0)) (fun Omega0 : gt n (Init.Nat.add (Init.Nat.mul (S (S O)) n) i) => @eq_ind_r Z Z0 (fun x : Z => forall _ : Z.ge x (Z.of_nat n), False) (fun _ : Z.ge Z0 (Z.of_nat n) => @ex_ind Z (fun y : Z => and (@eq Z (Z.of_nat n) y) (Z.le Z0 (Z.add (Z.mul y (Zpos xH)) Z0))) False (fun (Zvar2 : Z) (Omega16 : and (@eq Z (Z.of_nat n) Zvar2) (Z.le Z0 (Z.add (Z.mul Zvar2 (Zpos xH)) Z0))) => @and_ind (@eq Z (Z.of_nat n) Zvar2) (Z.le Z0 (Z.add (Z.mul Zvar2 (Zpos xH)) Z0)) False (fun (Omega9 : @eq Z (Z.of_nat n) Zvar2) (_ : Z.le Z0 (Z.add (Z.mul Zvar2 (Zpos xH)) Z0)) => @ex_ind Z (fun y : Z => and (@eq Z (Z.of_nat (Init.Nat.add (Init.Nat.mul (S (S O)) n) i)) y) (Z.le Z0 (Z.add (Z.mul y (Zpos xH)) Z0))) False (fun (Zvar3 : Z) (Omega15 : and (@eq Z (Z.of_nat (Init.Nat.add (Init.Nat.mul (S (S O)) n) i)) Zvar3) (Z.le Z0 (Z.add (Z.mul Zvar3 (Zpos xH)) Z0))) => @and_ind (@eq Z (Z.of_nat (Init.Nat.add (Init.Nat.mul (S (S O)) n) i)) Zvar3) (Z.le Z0 (Z.add (Z.mul Zvar3 (Zpos xH)) Z0)) False (fun (Omega11 : @eq Z (Z.of_nat (Init.Nat.add (Init.Nat.mul (S (S O)) n) i)) Zvar3) (_ : Z.le Z0 (Z.add (Z.mul Zvar3 (Zpos xH)) Z0)) => @eq_ind_r Z Zvar3 (fun x : Z => forall _ : Z.le Z0 (Z.add x (Z.opp (Z.of_nat n))), False) (@eq_ind_r Z Zvar2 (fun x : Z => forall _ : Z.le Z0 (Z.add Zvar3 (Z.opp x)), False) (fast_Zopp_eq_mult_neg_1 Zvar2 (fun x : Z => forall _ : Z.le Z0 (Z.add Zvar3 x), False) (fast_Zred_factor0 Zvar3 (fun x : Z => forall _ : Z.le Z0 (Z.add x (Z.mul Zvar2 (Zneg xH))), False) (fast_Zred_factor6 (Z.mul Zvar2 (Zneg xH)) (fun x : Z => forall _ : Z.le Z0 (Z.add (Z.mul Zvar3 (Zpos xH)) x), False) (fun Omega14 : Z.le Z0 (Z.add (Z.mul Zvar3 (Zpos xH)) (Z.add (Z.mul Zvar2 (Zneg xH)) Z0)) => @eq_ind_r Z Zvar2 (fun x : Z => forall _ : Z.le Z0 (Z.add (Z.add x (Zneg xH)) (Z.opp (Z.of_nat (Init.Nat.add (Init.Nat.mul (S (S O)) n) i)))), False) (@eq_ind_r Z Zvar3 (fun x : Z => forall _ : Z.le Z0 (Z.add (Z.add Zvar2 (Zneg xH)) (Z.opp x)), False) (fast_Zopp_eq_mult_neg_1 Zvar3 (fun x : Z => forall _ : Z.le Z0 (Z.add (Z.add Zvar2 (Zneg xH)) x), False) (fast_Zplus_comm (Z.add Zvar2 (Zneg xH)) (Z.mul Zvar3 (Zneg xH)) (fun x : Z => forall _ : Z.le Z0 x, False) (fast_Zred_factor0 Zvar2 (fun x : Z => forall _ : Z.le Z0 (Z.add (Z.mul Zvar3 (Zneg xH)) (Z.add x (Zneg xH))), False) (fun Omega12 : Z.le Z0 (Z.add (Z.mul Zvar3 (Zneg xH)) (Z.add (Z.mul Zvar2 (Zpos xH)) (Zneg xH))) => fast_OMEGA13 Zvar3 (Z.add (Z.mul Zvar2 (Zneg xH)) Z0) (Z.add (Z.mul Zvar2 (Zpos xH)) (Zneg xH)) xH (fun x : Z => forall _ : Z.le Z0 x, False) (fast_OMEGA14 Zvar2 Z0 (Zneg xH) xH (fun x : Z => forall _ : Z.le Z0 x, False) (fun H1 : not (@eq comparison Gt Gt) => False_ind False (H1 (@eq_refl comparison Gt)))) (OMEGA2 (Z.add (Z.mul Zvar3 (Zpos xH)) (Z.add (Z.mul Zvar2 (Zneg xH)) Z0)) (Z.add (Z.mul Zvar3 (Zneg xH)) (Z.add (Z.mul Zvar2 (Zpos xH)) (Zneg xH))) Omega14 Omega12))))) (Z.of_nat (Init.Nat.add (Init.Nat.mul (S (S O)) n) i)) Omega11) (Z.of_nat n) Omega9 (Zgt_left (Z.of_nat n) (Z.of_nat (Init.Nat.add (Init.Nat.mul (S (S O)) n) i)) (inj_gt n (Init.Nat.add (Init.Nat.mul (S (S O)) n) i) Omega0)))))) (Z.of_nat n) Omega9) (Z.of_nat (Init.Nat.add (Init.Nat.mul (S (S O)) n) i)) Omega11 (Zle_left (Z.of_nat n) (Z.of_nat (Init.Nat.add (Init.Nat.mul (S (S O)) n) i)) (inj_le n (Init.Nat.add (Init.Nat.mul (S (S O)) n) i) l))) Omega15) (intro_Z (Init.Nat.add (Init.Nat.mul (S (S O)) n) i))) Omega16) (intro_Z n)) (Z.of_nat (Init.Nat.sub (Init.Nat.add (Init.Nat.mul (S (S O)) n) i) n)) (inj_minus2 (Init.Nat.add (Init.Nat.mul (S (S O)) n) i) n Omega0)) (le_gt_dec n (Init.Nat.add (Init.Nat.mul (S (S O)) n) i)) (inj_ge (Init.Nat.sub (Init.Nat.add (Init.Nat.mul (S (S O)) n) i) n) n (not_lt (Init.Nat.sub (Init.Nat.add (Init.Nat.mul (S (S O)) n) i) n) n H))) (Z.of_nat (Init.Nat.mul (S (S O)) n)) (Nat2Z.inj_mul (S (S O)) n) (inj_lt (Init.Nat.add (Init.Nat.mul (S (S O)) n) i) (Init.Nat.mul (S (S O)) n) H2))))) O end (@sss_compute (mm_instr n) (vec nat n) (@mm_sss n) P (@pair nat (vec nat n) i v) (@pair nat (vec nat n) k (@vec_zero n))) *)
    destruct (le_lt_dec (2*n) (2*n+i)); [ | omega ].
(* Goal: iff (@sss_compute (mm_instr n) (vec nat n) (@mm_sss n) P (@pair nat (vec nat n) (Init.Nat.sub (Init.Nat.add (Init.Nat.mul (S (S O)) n) i) (Init.Nat.mul (S (S O)) n)) v) (@pair nat (vec nat n) k (@vec_zero n))) (@sss_compute (mm_instr n) (vec nat n) (@mm_sss n) P (@pair nat (vec nat n) i v) (@pair nat (vec nat n) k (@vec_zero n))) *)
    replace (2*n+i-2*n) with i by omega; tauto.
  Qed.

  Let H_s_rx : forall p v, s (rx p) v <-> v = vec_one p.
  Proof.
(* Goal: forall (p : pos n) (v : vec nat n), iff (s (rx p) v) (@eq (vec nat n) v (@vec_one n p)) *)
    intros p v; unfold s, rx.
(* Goal: iff match le_lt_dec n (@pos2nat n p) with | left H1 => match le_lt_dec (Init.Nat.mul (S (S O)) n) (@pos2nat n p) with | left l => @sss_compute (mm_instr n) (vec nat n) (@mm_sss n) P (@pair nat (vec nat n) (Init.Nat.sub (@pos2nat n p) (Init.Nat.mul (S (S O)) n)) v) (@pair nat (vec nat n) k (@vec_zero n)) | right H2 => @eq nat (@vec_pos nat n v (@nat2pos n (Init.Nat.sub (@pos2nat n p) n) (Decidable.dec_not_not (lt (Init.Nat.sub (@pos2nat n p) n) n) (dec_lt (Init.Nat.sub (@pos2nat n p) n) n) (fun H : not (lt (Init.Nat.sub (@pos2nat n p) n) n) => @eq_ind_r Z (Z.mul (Z.of_nat (S (S O))) (Z.of_nat n)) (fun x : Z => forall _ : Z.lt (Z.of_nat (@pos2nat n p)) x, False) (fun H3 : Z.lt (Z.of_nat (@pos2nat n p)) (Z.mul (Zpos (xO xH)) (Z.of_nat n)) => @sumbool_ind (le n (@pos2nat n p)) (gt n (@pos2nat n p)) (fun _ : sumbool (le n (@pos2nat n p)) (gt n (@pos2nat n p)) => forall _ : Z.ge (Z.of_nat (Init.Nat.sub (@pos2nat n p) n)) (Z.of_nat n), False) (fun Omega0 : le n (@pos2nat n p) => @eq_ind_r Z (Z.sub (Z.of_nat (@pos2nat n p)) (Z.of_nat n)) (fun x : Z => forall _ : Z.ge x (Z.of_nat n), False) (fun H0 : Z.ge (Z.sub (Z.of_nat (@pos2nat n p)) (Z.of_nat n)) (Z.of_nat n) => @ex_ind Z (fun y : Z => and (@eq Z (Z.of_nat (@pos2nat n p)) y) (Z.le Z0 (Z.add (Z.mul y (Zpos xH)) Z0))) False (fun (Zvar0 : Z) (Omega8 : and (@eq Z (Z.of_nat (@pos2nat n p)) Zvar0) (Z.le Z0 (Z.add (Z.mul Zvar0 (Zpos xH)) Z0))) => @and_ind (@eq Z (Z.of_nat (@pos2nat n p)) Zvar0) (Z.le Z0 (Z.add (Z.mul Zvar0 (Zpos xH)) Z0)) False (fun (Omega1 : @eq Z (Z.of_nat (@pos2nat n p)) Zvar0) (_ : Z.le Z0 (Z.add (Z.mul Zvar0 (Zpos xH)) Z0)) => @ex_ind Z (fun y : Z => and (@eq Z (Z.of_nat n) y) (Z.le Z0 (Z.add (Z.mul y (Zpos xH)) Z0))) False (fun (Zvar1 : Z) (Omega7 : and (@eq Z (Z.of_nat n) Zvar1) (Z.le Z0 (Z.add (Z.mul Zvar1 (Zpos xH)) Z0))) => @and_ind (@eq Z (Z.of_nat n) Zvar1) (Z.le Z0 (Z.add (Z.mul Zvar1 (Zpos xH)) Z0)) False (fun (Omega2 : @eq Z (Z.of_nat n) Zvar1) (_ : Z.le Z0 (Z.add (Z.mul Zvar1 (Zpos xH)) Z0)) => @eq_ind_r Z Zvar1 (fun x : Z => forall _ : Z.le Z0 (Z.add (Z.add (Z.mul (Zpos (xO xH)) x) (Zneg xH)) (Z.opp (Z.of_nat (@pos2nat n p)))), False) (fast_Zmult_comm (Zpos (xO xH)) Zvar1 (fun x : Z => forall _ : Z.le Z0 (Z.add (Z.add x (Zneg xH)) (Z.opp (Z.of_nat (@pos2nat n p)))), False) (@eq_ind_r Z Zvar0 (fun x : Z => forall _ : Z.le Z0 (Z.add (Z.add (Z.mul Zvar1 (Zpos (xO xH))) (Zneg xH)) (Z.opp x)), False) (fast_Zopp_eq_mult_neg_1 Zvar0 (fun x : Z => forall _ : Z.le Z0 (Z.add (Z.add (Z.mul Zvar1 (Zpos (xO xH))) (Zneg xH)) x), False) (fast_Zplus_comm (Z.add (Z.mul Zvar1 (Zpos (xO xH))) (Zneg xH)) (Z.mul Zvar0 (Zneg xH)) (fun x : Z => forall _ : Z.le Z0 x, False) (fun Omega5 : Z.le Z0 (Z.add (Z.mul Zvar0 (Zneg xH)) (Z.add (Z.mul Zvar1 (Zpos (xO xH))) (Zneg xH))) => @eq_ind_r Z Zvar0 (fun x : Z => forall _ : Z.le Z0 (Z.add (Z.add x (Z.opp (Z.of_nat n))) (Z.opp (Z.of_nat n))), False) (@eq_ind_r Z Zvar1 (fun x : Z => forall _ : Z.le Z0 (Z.add (Z.add Zvar0 (Z.opp x)) (Z.opp (Z.of_nat n))), False) (fast_Zopp_eq_mult_neg_1 Zvar1 (fun x : Z => forall _ : Z.le Z0 (Z.add (Z.add Zvar0 x) (Z.opp (Z.of_nat n))), False) (@eq_ind_r Z Zvar1 (fun x : Z => forall _ : Z.le Z0 (Z.add (Z.add Zvar0 (Z.mul Zvar1 (Zneg xH))) (Z.opp x)), False) (fast_Zopp_eq_mult_neg_1 Zvar1 (fun x : Z => forall _ : Z.le Z0 (Z.add (Z.add Zvar0 (Z.mul Zvar1 (Zneg xH))) x), False) (fast_Zplus_assoc_reverse Zvar0 (Z.mul Zvar1 (Zneg xH)) (Z.mul Zvar1 (Zneg xH)) (fun x : Z => forall _ : Z.le Z0 x, False) (fast_Zred_factor0 Zvar0 (fun x : Z => forall _ : Z.le Z0 (Z.add x (Z.add (Z.mul Zvar1 (Zneg xH)) (Z.mul Zvar1 (Zneg xH)))), False) (fast_Zred_factor4 Zvar1 (Zneg xH) (Zneg xH) (fun x : Z => forall _ : Z.le Z0 (Z.add (Z.mul Zvar0 (Zpos xH)) x), False) (fast_Zred_factor6 (Z.mul Zvar1 (Zneg (xO xH))) (fun x : Z => forall _ : Z.le Z0 (Z.add (Z.mul Zvar0 (Zpos xH)) x), False) (fun Omega3 : Z.le Z0 (Z.add (Z.mul Zvar0 (Zpos xH)) (Z.add (Z.mul Zvar1 (Zneg (xO xH))) Z0)) => fast_OMEGA13 Zvar0 (Z.add (Z.mul Zvar1 (Zneg (xO xH))) Z0) (Z.add (Z.mul Zvar1 (Zpos (xO xH))) (Zneg xH)) xH (fun x : Z => forall _ : Z.le Z0 x, False) (fast_OMEGA14 Zvar1 Z0 (Zneg xH) (xO xH) (fun x : Z => forall _ : Z.le Z0 x, False) (fun H4 : not (@eq comparison Gt Gt) => False_ind False (H4 (@eq_refl comparison Gt)))) (OMEGA2 (Z.add (Z.mul Zvar0 (Zpos xH)) (Z.add (Z.mul Zvar1 (Zneg (xO xH))) Z0)) (Z.add (Z.mul Zvar0 (Zneg xH)) (Z.add (Z.mul Zvar1 (Zpos (xO xH))) (Zneg xH))) Omega3 Omega5))))))) (Z.of_nat n) Omega2)) (Z.of_nat n) Omega2) (Z.of_nat (@pos2nat n p)) Omega1 (Zge_left (Z.sub (Z.of_nat (@pos2nat n p)) (Z.of_nat n)) (Z.of_nat n) H0)))) (Z.of_nat (@pos2nat n p)) Omega1)) (Z.of_nat n) Omega2 (Zlt_left (Z.of_nat (@pos2nat n p)) (Z.mul (Zpos (xO xH)) (Z.of_nat n)) H3)) Omega7) (intro_Z n)) Omega8) (intro_Z (@pos2nat n p))) (Z.of_nat (Init.Nat.sub (@pos2nat n p) n)) (Nat2Z.inj_sub (@pos2nat n p) n Omega0)) (fun Omega0 : gt n (@pos2nat n p) => @eq_ind_r Z Z0 (fun x : Z => forall _ : Z.ge x (Z.of_nat n), False) (fun _ : Z.ge Z0 (Z.of_nat n) => @ex_ind Z (fun y : Z => and (@eq Z (Z.of_nat n) y) (Z.le Z0 (Z.add (Z.mul y (Zpos xH)) Z0))) False (fun (Zvar2 : Z) (Omega16 : and (@eq Z (Z.of_nat n) Zvar2) (Z.le Z0 (Z.add (Z.mul Zvar2 (Zpos xH)) Z0))) => @and_ind (@eq Z (Z.of_nat n) Zvar2) (Z.le Z0 (Z.add (Z.mul Zvar2 (Zpos xH)) Z0)) False (fun (Omega9 : @eq Z (Z.of_nat n) Zvar2) (_ : Z.le Z0 (Z.add (Z.mul Zvar2 (Zpos xH)) Z0)) => @ex_ind Z (fun y : Z => and (@eq Z (Z.of_nat (@pos2nat n p)) y) (Z.le Z0 (Z.add (Z.mul y (Zpos xH)) Z0))) False (fun (Zvar3 : Z) (Omega15 : and (@eq Z (Z.of_nat (@pos2nat n p)) Zvar3) (Z.le Z0 (Z.add (Z.mul Zvar3 (Zpos xH)) Z0))) => @and_ind (@eq Z (Z.of_nat (@pos2nat n p)) Zvar3) (Z.le Z0 (Z.add (Z.mul Zvar3 (Zpos xH)) Z0)) False (fun (Omega11 : @eq Z (Z.of_nat (@pos2nat n p)) Zvar3) (_ : Z.le Z0 (Z.add (Z.mul Zvar3 (Zpos xH)) Z0)) => @eq_ind_r Z Zvar3 (fun x : Z => forall _ : Z.le Z0 (Z.add x (Z.opp (Z.of_nat n))), False) (@eq_ind_r Z Zvar2 (fun x : Z => forall _ : Z.le Z0 (Z.add Zvar3 (Z.opp x)), False) (fast_Zopp_eq_mult_neg_1 Zvar2 (fun x : Z => forall _ : Z.le Z0 (Z.add Zvar3 x), False) (fast_Zred_factor0 Zvar3 (fun x : Z => forall _ : Z.le Z0 (Z.add x (Z.mul Zvar2 (Zneg xH))), False) (fast_Zred_factor6 (Z.mul Zvar2 (Zneg xH)) (fun x : Z => forall _ : Z.le Z0 (Z.add (Z.mul Zvar3 (Zpos xH)) x), False) (fun Omega14 : Z.le Z0 (Z.add (Z.mul Zvar3 (Zpos xH)) (Z.add (Z.mul Zvar2 (Zneg xH)) Z0)) => @eq_ind_r Z Zvar2 (fun x : Z => forall _ : Z.le Z0 (Z.add (Z.add x (Zneg xH)) (Z.opp (Z.of_nat (@pos2nat n p)))), False) (@eq_ind_r Z Zvar3 (fun x : Z => forall _ : Z.le Z0 (Z.add (Z.add Zvar2 (Zneg xH)) (Z.opp x)), False) (fast_Zopp_eq_mult_neg_1 Zvar3 (fun x : Z => forall _ : Z.le Z0 (Z.add (Z.add Zvar2 (Zneg xH)) x), False) (fast_Zplus_comm (Z.add Zvar2 (Zneg xH)) (Z.mul Zvar3 (Zneg xH)) (fun x : Z => forall _ : Z.le Z0 x, False) (fast_Zred_factor0 Zvar2 (fun x : Z => forall _ : Z.le Z0 (Z.add (Z.mul Zvar3 (Zneg xH)) (Z.add x (Zneg xH))), False) (fun Omega12 : Z.le Z0 (Z.add (Z.mul Zvar3 (Zneg xH)) (Z.add (Z.mul Zvar2 (Zpos xH)) (Zneg xH))) => fast_OMEGA13 Zvar3 (Z.add (Z.mul Zvar2 (Zneg xH)) Z0) (Z.add (Z.mul Zvar2 (Zpos xH)) (Zneg xH)) xH (fun x : Z => forall _ : Z.le Z0 x, False) (fast_OMEGA14 Zvar2 Z0 (Zneg xH) xH (fun x : Z => forall _ : Z.le Z0 x, False) (fun H4 : not (@eq comparison Gt Gt) => False_ind False (H4 (@eq_refl comparison Gt)))) (OMEGA2 (Z.add (Z.mul Zvar3 (Zpos xH)) (Z.add (Z.mul Zvar2 (Zneg xH)) Z0)) (Z.add (Z.mul Zvar3 (Zneg xH)) (Z.add (Z.mul Zvar2 (Zpos xH)) (Zneg xH))) Omega14 Omega12))))) (Z.of_nat (@pos2nat n p)) Omega11) (Z.of_nat n) Omega9 (Zgt_left (Z.of_nat n) (Z.of_nat (@pos2nat n p)) (inj_gt n (@pos2nat n p) Omega0)))))) (Z.of_nat n) Omega9) (Z.of_nat (@pos2nat n p)) Omega11 (Zle_left (Z.of_nat n) (Z.of_nat (@pos2nat n p)) (inj_le n (@pos2nat n p) H1))) Omega15) (intro_Z (@pos2nat n p))) Omega16) (intro_Z n)) (Z.of_nat (Init.Nat.sub (@pos2nat n p) n)) (inj_minus2 (@pos2nat n p) n Omega0)) (le_gt_dec n (@pos2nat n p)) (inj_ge (Init.Nat.sub (@pos2nat n p) n) n (not_lt (Init.Nat.sub (@pos2nat n p) n) n H))) (Z.of_nat (Init.Nat.mul (S (S O)) n)) (Nat2Z.inj_mul (S (S O)) n) (inj_lt (@pos2nat n p) (Init.Nat.mul (S (S O)) n) H2))))) O end | right H1 => @eq (vec nat n) v (@vec_one n (@nat2pos n (@pos2nat n p) H1)) end (@eq (vec nat n) v (@vec_one n p)) *)
    destruct (le_lt_dec n (pos2nat p)).
(* Goal: iff (@sss_compute (mm_instr n) (vec nat n) (@mm_sss n) P (@pair nat (vec nat n) (Init.Nat.sub (Init.Nat.add n (@pos2nat n p)) (Init.Nat.mul (S (S O)) n)) v) (@pair nat (vec nat n) k (@vec_zero n))) (@eq nat (@vec_pos nat n v p) O) *)
(* Goal: iff (@eq nat (@vec_pos nat n v (@nat2pos n (Init.Nat.sub (Init.Nat.add n (@pos2nat n p)) n) (Decidable.dec_not_not (lt (Init.Nat.sub (Init.Nat.add n (@pos2nat n p)) n) n) (dec_lt (Init.Nat.sub (Init.Nat.add n (@pos2nat n p)) n) n) (fun H : not (lt (Init.Nat.sub (Init.Nat.add n (@pos2nat n p)) n) n) => @eq_ind_r Z (Z.mul (Z.of_nat (S (S O))) (Z.of_nat n)) (fun x : Z => forall _ : Z.lt (Z.of_nat (Init.Nat.add n (@pos2nat n p))) x, False) (fun H2 : Z.lt (Z.of_nat (Init.Nat.add n (@pos2nat n p))) (Z.mul (Zpos (xO xH)) (Z.of_nat n)) => @sumbool_ind (le n (Init.Nat.add n (@pos2nat n p))) (gt n (Init.Nat.add n (@pos2nat n p))) (fun _ : sumbool (le n (Init.Nat.add n (@pos2nat n p))) (gt n (Init.Nat.add n (@pos2nat n p))) => forall _ : Z.ge (Z.of_nat (Init.Nat.sub (Init.Nat.add n (@pos2nat n p)) n)) (Z.of_nat n), False) (fun Omega0 : le n (Init.Nat.add n (@pos2nat n p)) => @eq_ind_r Z (Z.sub (Z.of_nat (Init.Nat.add n (@pos2nat n p))) (Z.of_nat n)) (fun x : Z => forall _ : Z.ge x (Z.of_nat n), False) (fun H0 : Z.ge (Z.sub (Z.of_nat (Init.Nat.add n (@pos2nat n p))) (Z.of_nat n)) (Z.of_nat n) => @ex_ind Z (fun y : Z => and (@eq Z (Z.of_nat (Init.Nat.add n (@pos2nat n p))) y) (Z.le Z0 (Z.add (Z.mul y (Zpos xH)) Z0))) False (fun (Zvar0 : Z) (Omega8 : and (@eq Z (Z.of_nat (Init.Nat.add n (@pos2nat n p))) Zvar0) (Z.le Z0 (Z.add (Z.mul Zvar0 (Zpos xH)) Z0))) => @and_ind (@eq Z (Z.of_nat (Init.Nat.add n (@pos2nat n p))) Zvar0) (Z.le Z0 (Z.add (Z.mul Zvar0 (Zpos xH)) Z0)) False (fun (Omega1 : @eq Z (Z.of_nat (Init.Nat.add n (@pos2nat n p))) Zvar0) (_ : Z.le Z0 (Z.add (Z.mul Zvar0 (Zpos xH)) Z0)) => @ex_ind Z (fun y : Z => and (@eq Z (Z.of_nat n) y) (Z.le Z0 (Z.add (Z.mul y (Zpos xH)) Z0))) False (fun (Zvar1 : Z) (Omega7 : and (@eq Z (Z.of_nat n) Zvar1) (Z.le Z0 (Z.add (Z.mul Zvar1 (Zpos xH)) Z0))) => @and_ind (@eq Z (Z.of_nat n) Zvar1) (Z.le Z0 (Z.add (Z.mul Zvar1 (Zpos xH)) Z0)) False (fun (Omega2 : @eq Z (Z.of_nat n) Zvar1) (_ : Z.le Z0 (Z.add (Z.mul Zvar1 (Zpos xH)) Z0)) => @eq_ind_r Z Zvar1 (fun x : Z => forall _ : Z.le Z0 (Z.add (Z.add (Z.mul (Zpos (xO xH)) x) (Zneg xH)) (Z.opp (Z.of_nat (Init.Nat.add n (@pos2nat n p))))), False) (fast_Zmult_comm (Zpos (xO xH)) Zvar1 (fun x : Z => forall _ : Z.le Z0 (Z.add (Z.add x (Zneg xH)) (Z.opp (Z.of_nat (Init.Nat.add n (@pos2nat n p))))), False) (@eq_ind_r Z Zvar0 (fun x : Z => forall _ : Z.le Z0 (Z.add (Z.add (Z.mul Zvar1 (Zpos (xO xH))) (Zneg xH)) (Z.opp x)), False) (fast_Zopp_eq_mult_neg_1 Zvar0 (fun x : Z => forall _ : Z.le Z0 (Z.add (Z.add (Z.mul Zvar1 (Zpos (xO xH))) (Zneg xH)) x), False) (fast_Zplus_comm (Z.add (Z.mul Zvar1 (Zpos (xO xH))) (Zneg xH)) (Z.mul Zvar0 (Zneg xH)) (fun x : Z => forall _ : Z.le Z0 x, False) (fun Omega5 : Z.le Z0 (Z.add (Z.mul Zvar0 (Zneg xH)) (Z.add (Z.mul Zvar1 (Zpos (xO xH))) (Zneg xH))) => @eq_ind_r Z Zvar0 (fun x : Z => forall _ : Z.le Z0 (Z.add (Z.add x (Z.opp (Z.of_nat n))) (Z.opp (Z.of_nat n))), False) (@eq_ind_r Z Zvar1 (fun x : Z => forall _ : Z.le Z0 (Z.add (Z.add Zvar0 (Z.opp x)) (Z.opp (Z.of_nat n))), False) (fast_Zopp_eq_mult_neg_1 Zvar1 (fun x : Z => forall _ : Z.le Z0 (Z.add (Z.add Zvar0 x) (Z.opp (Z.of_nat n))), False) (@eq_ind_r Z Zvar1 (fun x : Z => forall _ : Z.le Z0 (Z.add (Z.add Zvar0 (Z.mul Zvar1 (Zneg xH))) (Z.opp x)), False) (fast_Zopp_eq_mult_neg_1 Zvar1 (fun x : Z => forall _ : Z.le Z0 (Z.add (Z.add Zvar0 (Z.mul Zvar1 (Zneg xH))) x), False) (fast_Zplus_assoc_reverse Zvar0 (Z.mul Zvar1 (Zneg xH)) (Z.mul Zvar1 (Zneg xH)) (fun x : Z => forall _ : Z.le Z0 x, False) (fast_Zred_factor0 Zvar0 (fun x : Z => forall _ : Z.le Z0 (Z.add x (Z.add (Z.mul Zvar1 (Zneg xH)) (Z.mul Zvar1 (Zneg xH)))), False) (fast_Zred_factor4 Zvar1 (Zneg xH) (Zneg xH) (fun x : Z => forall _ : Z.le Z0 (Z.add (Z.mul Zvar0 (Zpos xH)) x), False) (fast_Zred_factor6 (Z.mul Zvar1 (Zneg (xO xH))) (fun x : Z => forall _ : Z.le Z0 (Z.add (Z.mul Zvar0 (Zpos xH)) x), False) (fun Omega3 : Z.le Z0 (Z.add (Z.mul Zvar0 (Zpos xH)) (Z.add (Z.mul Zvar1 (Zneg (xO xH))) Z0)) => fast_OMEGA13 Zvar0 (Z.add (Z.mul Zvar1 (Zneg (xO xH))) Z0) (Z.add (Z.mul Zvar1 (Zpos (xO xH))) (Zneg xH)) xH (fun x : Z => forall _ : Z.le Z0 x, False) (fast_OMEGA14 Zvar1 Z0 (Zneg xH) (xO xH) (fun x : Z => forall _ : Z.le Z0 x, False) (fun H1 : not (@eq comparison Gt Gt) => False_ind False (H1 (@eq_refl comparison Gt)))) (OMEGA2 (Z.add (Z.mul Zvar0 (Zpos xH)) (Z.add (Z.mul Zvar1 (Zneg (xO xH))) Z0)) (Z.add (Z.mul Zvar0 (Zneg xH)) (Z.add (Z.mul Zvar1 (Zpos (xO xH))) (Zneg xH))) Omega3 Omega5))))))) (Z.of_nat n) Omega2)) (Z.of_nat n) Omega2) (Z.of_nat (Init.Nat.add n (@pos2nat n p))) Omega1 (Zge_left (Z.sub (Z.of_nat (Init.Nat.add n (@pos2nat n p))) (Z.of_nat n)) (Z.of_nat n) H0)))) (Z.of_nat (Init.Nat.add n (@pos2nat n p))) Omega1)) (Z.of_nat n) Omega2 (Zlt_left (Z.of_nat (Init.Nat.add n (@pos2nat n p))) (Z.mul (Zpos (xO xH)) (Z.of_nat n)) H2)) Omega7) (intro_Z n)) Omega8) (intro_Z (Init.Nat.add n (@pos2nat n p)))) (Z.of_nat (Init.Nat.sub (Init.Nat.add n (@pos2nat n p)) n)) (Nat2Z.inj_sub (Init.Nat.add n (@pos2nat n p)) n Omega0)) (fun Omega0 : gt n (Init.Nat.add n (@pos2nat n p)) => @eq_ind_r Z Z0 (fun x : Z => forall _ : Z.ge x (Z.of_nat n), False) (fun _ : Z.ge Z0 (Z.of_nat n) => @ex_ind Z (fun y : Z => and (@eq Z (Z.of_nat n) y) (Z.le Z0 (Z.add (Z.mul y (Zpos xH)) Z0))) False (fun (Zvar2 : Z) (Omega16 : and (@eq Z (Z.of_nat n) Zvar2) (Z.le Z0 (Z.add (Z.mul Zvar2 (Zpos xH)) Z0))) => @and_ind (@eq Z (Z.of_nat n) Zvar2) (Z.le Z0 (Z.add (Z.mul Zvar2 (Zpos xH)) Z0)) False (fun (Omega9 : @eq Z (Z.of_nat n) Zvar2) (_ : Z.le Z0 (Z.add (Z.mul Zvar2 (Zpos xH)) Z0)) => @ex_ind Z (fun y : Z => and (@eq Z (Z.of_nat (Init.Nat.add n (@pos2nat n p))) y) (Z.le Z0 (Z.add (Z.mul y (Zpos xH)) Z0))) False (fun (Zvar3 : Z) (Omega15 : and (@eq Z (Z.of_nat (Init.Nat.add n (@pos2nat n p))) Zvar3) (Z.le Z0 (Z.add (Z.mul Zvar3 (Zpos xH)) Z0))) => @and_ind (@eq Z (Z.of_nat (Init.Nat.add n (@pos2nat n p))) Zvar3) (Z.le Z0 (Z.add (Z.mul Zvar3 (Zpos xH)) Z0)) False (fun (Omega11 : @eq Z (Z.of_nat (Init.Nat.add n (@pos2nat n p))) Zvar3) (_ : Z.le Z0 (Z.add (Z.mul Zvar3 (Zpos xH)) Z0)) => @eq_ind_r Z Zvar3 (fun x : Z => forall _ : Z.le Z0 (Z.add x (Z.opp (Z.of_nat n))), False) (@eq_ind_r Z Zvar2 (fun x : Z => forall _ : Z.le Z0 (Z.add Zvar3 (Z.opp x)), False) (fast_Zopp_eq_mult_neg_1 Zvar2 (fun x : Z => forall _ : Z.le Z0 (Z.add Zvar3 x), False) (fast_Zred_factor0 Zvar3 (fun x : Z => forall _ : Z.le Z0 (Z.add x (Z.mul Zvar2 (Zneg xH))), False) (fast_Zred_factor6 (Z.mul Zvar2 (Zneg xH)) (fun x : Z => forall _ : Z.le Z0 (Z.add (Z.mul Zvar3 (Zpos xH)) x), False) (fun Omega14 : Z.le Z0 (Z.add (Z.mul Zvar3 (Zpos xH)) (Z.add (Z.mul Zvar2 (Zneg xH)) Z0)) => @eq_ind_r Z Zvar2 (fun x : Z => forall _ : Z.le Z0 (Z.add (Z.add x (Zneg xH)) (Z.opp (Z.of_nat (Init.Nat.add n (@pos2nat n p))))), False) (@eq_ind_r Z Zvar3 (fun x : Z => forall _ : Z.le Z0 (Z.add (Z.add Zvar2 (Zneg xH)) (Z.opp x)), False) (fast_Zopp_eq_mult_neg_1 Zvar3 (fun x : Z => forall _ : Z.le Z0 (Z.add (Z.add Zvar2 (Zneg xH)) x), False) (fast_Zplus_comm (Z.add Zvar2 (Zneg xH)) (Z.mul Zvar3 (Zneg xH)) (fun x : Z => forall _ : Z.le Z0 x, False) (fast_Zred_factor0 Zvar2 (fun x : Z => forall _ : Z.le Z0 (Z.add (Z.mul Zvar3 (Zneg xH)) (Z.add x (Zneg xH))), False) (fun Omega12 : Z.le Z0 (Z.add (Z.mul Zvar3 (Zneg xH)) (Z.add (Z.mul Zvar2 (Zpos xH)) (Zneg xH))) => fast_OMEGA13 Zvar3 (Z.add (Z.mul Zvar2 (Zneg xH)) Z0) (Z.add (Z.mul Zvar2 (Zpos xH)) (Zneg xH)) xH (fun x : Z => forall _ : Z.le Z0 x, False) (fast_OMEGA14 Zvar2 Z0 (Zneg xH) xH (fun x : Z => forall _ : Z.le Z0 x, False) (fun H1 : not (@eq comparison Gt Gt) => False_ind False (H1 (@eq_refl comparison Gt)))) (OMEGA2 (Z.add (Z.mul Zvar3 (Zpos xH)) (Z.add (Z.mul Zvar2 (Zneg xH)) Z0)) (Z.add (Z.mul Zvar3 (Zneg xH)) (Z.add (Z.mul Zvar2 (Zpos xH)) (Zneg xH))) Omega14 Omega12))))) (Z.of_nat (Init.Nat.add n (@pos2nat n p))) Omega11) (Z.of_nat n) Omega9 (Zgt_left (Z.of_nat n) (Z.of_nat (Init.Nat.add n (@pos2nat n p))) (inj_gt n (Init.Nat.add n (@pos2nat n p)) Omega0)))))) (Z.of_nat n) Omega9) (Z.of_nat (Init.Nat.add n (@pos2nat n p))) Omega11 (Zle_left (Z.of_nat n) (Z.of_nat (Init.Nat.add n (@pos2nat n p))) (inj_le n (Init.Nat.add n (@pos2nat n p)) l))) Omega15) (intro_Z (Init.Nat.add n (@pos2nat n p)))) Omega16) (intro_Z n)) (Z.of_nat (Init.Nat.sub (Init.Nat.add n (@pos2nat n p)) n)) (inj_minus2 (Init.Nat.add n (@pos2nat n p)) n Omega0)) (le_gt_dec n (Init.Nat.add n (@pos2nat n p))) (inj_ge (Init.Nat.sub (Init.Nat.add n (@pos2nat n p)) n) n (not_lt (Init.Nat.sub (Init.Nat.add n (@pos2nat n p)) n) n H))) (Z.of_nat (Init.Nat.mul (S (S O)) n)) (Nat2Z.inj_mul (S (S O)) n) (inj_lt (Init.Nat.add n (@pos2nat n p)) (Init.Nat.mul (S (S O)) n) l0))))) O) (@eq nat (@vec_pos nat n v p) O) *)
    generalize (pos2nat_prop p); omega.
(* Goal: iff (@eq (vec nat n) v (@vec_one n (@nat2pos n (@pos2nat n p) l))) (@eq (vec nat n) v (@vec_one n p)) *)
    rewrite nat2pos_pos2nat; tauto.
  Qed.
 
  Let H_s_ry : forall p v, s (ry p) v <-> vec_pos v p = 0.
  Proof.
(* Goal: forall (p : pos n) (v : vec nat n), iff (s (ry p) v) (@eq nat (@vec_pos nat n v p) O) *)
    intros p v; unfold s, ry.
(* Goal: iff match le_lt_dec n (Init.Nat.add n (@pos2nat n p)) with | left H1 => match le_lt_dec (Init.Nat.mul (S (S O)) n) (Init.Nat.add n (@pos2nat n p)) with | left l => @sss_compute (mm_instr n) (vec nat n) (@mm_sss n) P (@pair nat (vec nat n) (Init.Nat.sub (Init.Nat.add n (@pos2nat n p)) (Init.Nat.mul (S (S O)) n)) v) (@pair nat (vec nat n) k (@vec_zero n)) | right H2 => @eq nat (@vec_pos nat n v (@nat2pos n (Init.Nat.sub (Init.Nat.add n (@pos2nat n p)) n) (Decidable.dec_not_not (lt (Init.Nat.sub (Init.Nat.add n (@pos2nat n p)) n) n) (dec_lt (Init.Nat.sub (Init.Nat.add n (@pos2nat n p)) n) n) (fun H : not (lt (Init.Nat.sub (Init.Nat.add n (@pos2nat n p)) n) n) => @eq_ind_r Z (Z.mul (Z.of_nat (S (S O))) (Z.of_nat n)) (fun x : Z => forall _ : Z.lt (Z.of_nat (Init.Nat.add n (@pos2nat n p))) x, False) (fun H3 : Z.lt (Z.of_nat (Init.Nat.add n (@pos2nat n p))) (Z.mul (Zpos (xO xH)) (Z.of_nat n)) => @sumbool_ind (le n (Init.Nat.add n (@pos2nat n p))) (gt n (Init.Nat.add n (@pos2nat n p))) (fun _ : sumbool (le n (Init.Nat.add n (@pos2nat n p))) (gt n (Init.Nat.add n (@pos2nat n p))) => forall _ : Z.ge (Z.of_nat (Init.Nat.sub (Init.Nat.add n (@pos2nat n p)) n)) (Z.of_nat n), False) (fun Omega0 : le n (Init.Nat.add n (@pos2nat n p)) => @eq_ind_r Z (Z.sub (Z.of_nat (Init.Nat.add n (@pos2nat n p))) (Z.of_nat n)) (fun x : Z => forall _ : Z.ge x (Z.of_nat n), False) (fun H0 : Z.ge (Z.sub (Z.of_nat (Init.Nat.add n (@pos2nat n p))) (Z.of_nat n)) (Z.of_nat n) => @ex_ind Z (fun y : Z => and (@eq Z (Z.of_nat (Init.Nat.add n (@pos2nat n p))) y) (Z.le Z0 (Z.add (Z.mul y (Zpos xH)) Z0))) False (fun (Zvar0 : Z) (Omega8 : and (@eq Z (Z.of_nat (Init.Nat.add n (@pos2nat n p))) Zvar0) (Z.le Z0 (Z.add (Z.mul Zvar0 (Zpos xH)) Z0))) => @and_ind (@eq Z (Z.of_nat (Init.Nat.add n (@pos2nat n p))) Zvar0) (Z.le Z0 (Z.add (Z.mul Zvar0 (Zpos xH)) Z0)) False (fun (Omega1 : @eq Z (Z.of_nat (Init.Nat.add n (@pos2nat n p))) Zvar0) (_ : Z.le Z0 (Z.add (Z.mul Zvar0 (Zpos xH)) Z0)) => @ex_ind Z (fun y : Z => and (@eq Z (Z.of_nat n) y) (Z.le Z0 (Z.add (Z.mul y (Zpos xH)) Z0))) False (fun (Zvar1 : Z) (Omega7 : and (@eq Z (Z.of_nat n) Zvar1) (Z.le Z0 (Z.add (Z.mul Zvar1 (Zpos xH)) Z0))) => @and_ind (@eq Z (Z.of_nat n) Zvar1) (Z.le Z0 (Z.add (Z.mul Zvar1 (Zpos xH)) Z0)) False (fun (Omega2 : @eq Z (Z.of_nat n) Zvar1) (_ : Z.le Z0 (Z.add (Z.mul Zvar1 (Zpos xH)) Z0)) => @eq_ind_r Z Zvar1 (fun x : Z => forall _ : Z.le Z0 (Z.add (Z.add (Z.mul (Zpos (xO xH)) x) (Zneg xH)) (Z.opp (Z.of_nat (Init.Nat.add n (@pos2nat n p))))), False) (fast_Zmult_comm (Zpos (xO xH)) Zvar1 (fun x : Z => forall _ : Z.le Z0 (Z.add (Z.add x (Zneg xH)) (Z.opp (Z.of_nat (Init.Nat.add n (@pos2nat n p))))), False) (@eq_ind_r Z Zvar0 (fun x : Z => forall _ : Z.le Z0 (Z.add (Z.add (Z.mul Zvar1 (Zpos (xO xH))) (Zneg xH)) (Z.opp x)), False) (fast_Zopp_eq_mult_neg_1 Zvar0 (fun x : Z => forall _ : Z.le Z0 (Z.add (Z.add (Z.mul Zvar1 (Zpos (xO xH))) (Zneg xH)) x), False) (fast_Zplus_comm (Z.add (Z.mul Zvar1 (Zpos (xO xH))) (Zneg xH)) (Z.mul Zvar0 (Zneg xH)) (fun x : Z => forall _ : Z.le Z0 x, False) (fun Omega5 : Z.le Z0 (Z.add (Z.mul Zvar0 (Zneg xH)) (Z.add (Z.mul Zvar1 (Zpos (xO xH))) (Zneg xH))) => @eq_ind_r Z Zvar0 (fun x : Z => forall _ : Z.le Z0 (Z.add (Z.add x (Z.opp (Z.of_nat n))) (Z.opp (Z.of_nat n))), False) (@eq_ind_r Z Zvar1 (fun x : Z => forall _ : Z.le Z0 (Z.add (Z.add Zvar0 (Z.opp x)) (Z.opp (Z.of_nat n))), False) (fast_Zopp_eq_mult_neg_1 Zvar1 (fun x : Z => forall _ : Z.le Z0 (Z.add (Z.add Zvar0 x) (Z.opp (Z.of_nat n))), False) (@eq_ind_r Z Zvar1 (fun x : Z => forall _ : Z.le Z0 (Z.add (Z.add Zvar0 (Z.mul Zvar1 (Zneg xH))) (Z.opp x)), False) (fast_Zopp_eq_mult_neg_1 Zvar1 (fun x : Z => forall _ : Z.le Z0 (Z.add (Z.add Zvar0 (Z.mul Zvar1 (Zneg xH))) x), False) (fast_Zplus_assoc_reverse Zvar0 (Z.mul Zvar1 (Zneg xH)) (Z.mul Zvar1 (Zneg xH)) (fun x : Z => forall _ : Z.le Z0 x, False) (fast_Zred_factor0 Zvar0 (fun x : Z => forall _ : Z.le Z0 (Z.add x (Z.add (Z.mul Zvar1 (Zneg xH)) (Z.mul Zvar1 (Zneg xH)))), False) (fast_Zred_factor4 Zvar1 (Zneg xH) (Zneg xH) (fun x : Z => forall _ : Z.le Z0 (Z.add (Z.mul Zvar0 (Zpos xH)) x), False) (fast_Zred_factor6 (Z.mul Zvar1 (Zneg (xO xH))) (fun x : Z => forall _ : Z.le Z0 (Z.add (Z.mul Zvar0 (Zpos xH)) x), False) (fun Omega3 : Z.le Z0 (Z.add (Z.mul Zvar0 (Zpos xH)) (Z.add (Z.mul Zvar1 (Zneg (xO xH))) Z0)) => fast_OMEGA13 Zvar0 (Z.add (Z.mul Zvar1 (Zneg (xO xH))) Z0) (Z.add (Z.mul Zvar1 (Zpos (xO xH))) (Zneg xH)) xH (fun x : Z => forall _ : Z.le Z0 x, False) (fast_OMEGA14 Zvar1 Z0 (Zneg xH) (xO xH) (fun x : Z => forall _ : Z.le Z0 x, False) (fun H4 : not (@eq comparison Gt Gt) => False_ind False (H4 (@eq_refl comparison Gt)))) (OMEGA2 (Z.add (Z.mul Zvar0 (Zpos xH)) (Z.add (Z.mul Zvar1 (Zneg (xO xH))) Z0)) (Z.add (Z.mul Zvar0 (Zneg xH)) (Z.add (Z.mul Zvar1 (Zpos (xO xH))) (Zneg xH))) Omega3 Omega5))))))) (Z.of_nat n) Omega2)) (Z.of_nat n) Omega2) (Z.of_nat (Init.Nat.add n (@pos2nat n p))) Omega1 (Zge_left (Z.sub (Z.of_nat (Init.Nat.add n (@pos2nat n p))) (Z.of_nat n)) (Z.of_nat n) H0)))) (Z.of_nat (Init.Nat.add n (@pos2nat n p))) Omega1)) (Z.of_nat n) Omega2 (Zlt_left (Z.of_nat (Init.Nat.add n (@pos2nat n p))) (Z.mul (Zpos (xO xH)) (Z.of_nat n)) H3)) Omega7) (intro_Z n)) Omega8) (intro_Z (Init.Nat.add n (@pos2nat n p)))) (Z.of_nat (Init.Nat.sub (Init.Nat.add n (@pos2nat n p)) n)) (Nat2Z.inj_sub (Init.Nat.add n (@pos2nat n p)) n Omega0)) (fun Omega0 : gt n (Init.Nat.add n (@pos2nat n p)) => @eq_ind_r Z Z0 (fun x : Z => forall _ : Z.ge x (Z.of_nat n), False) (fun _ : Z.ge Z0 (Z.of_nat n) => @ex_ind Z (fun y : Z => and (@eq Z (Z.of_nat n) y) (Z.le Z0 (Z.add (Z.mul y (Zpos xH)) Z0))) False (fun (Zvar2 : Z) (Omega16 : and (@eq Z (Z.of_nat n) Zvar2) (Z.le Z0 (Z.add (Z.mul Zvar2 (Zpos xH)) Z0))) => @and_ind (@eq Z (Z.of_nat n) Zvar2) (Z.le Z0 (Z.add (Z.mul Zvar2 (Zpos xH)) Z0)) False (fun (Omega9 : @eq Z (Z.of_nat n) Zvar2) (_ : Z.le Z0 (Z.add (Z.mul Zvar2 (Zpos xH)) Z0)) => @ex_ind Z (fun y : Z => and (@eq Z (Z.of_nat (Init.Nat.add n (@pos2nat n p))) y) (Z.le Z0 (Z.add (Z.mul y (Zpos xH)) Z0))) False (fun (Zvar3 : Z) (Omega15 : and (@eq Z (Z.of_nat (Init.Nat.add n (@pos2nat n p))) Zvar3) (Z.le Z0 (Z.add (Z.mul Zvar3 (Zpos xH)) Z0))) => @and_ind (@eq Z (Z.of_nat (Init.Nat.add n (@pos2nat n p))) Zvar3) (Z.le Z0 (Z.add (Z.mul Zvar3 (Zpos xH)) Z0)) False (fun (Omega11 : @eq Z (Z.of_nat (Init.Nat.add n (@pos2nat n p))) Zvar3) (_ : Z.le Z0 (Z.add (Z.mul Zvar3 (Zpos xH)) Z0)) => @eq_ind_r Z Zvar3 (fun x : Z => forall _ : Z.le Z0 (Z.add x (Z.opp (Z.of_nat n))), False) (@eq_ind_r Z Zvar2 (fun x : Z => forall _ : Z.le Z0 (Z.add Zvar3 (Z.opp x)), False) (fast_Zopp_eq_mult_neg_1 Zvar2 (fun x : Z => forall _ : Z.le Z0 (Z.add Zvar3 x), False) (fast_Zred_factor0 Zvar3 (fun x : Z => forall _ : Z.le Z0 (Z.add x (Z.mul Zvar2 (Zneg xH))), False) (fast_Zred_factor6 (Z.mul Zvar2 (Zneg xH)) (fun x : Z => forall _ : Z.le Z0 (Z.add (Z.mul Zvar3 (Zpos xH)) x), False) (fun Omega14 : Z.le Z0 (Z.add (Z.mul Zvar3 (Zpos xH)) (Z.add (Z.mul Zvar2 (Zneg xH)) Z0)) => @eq_ind_r Z Zvar2 (fun x : Z => forall _ : Z.le Z0 (Z.add (Z.add x (Zneg xH)) (Z.opp (Z.of_nat (Init.Nat.add n (@pos2nat n p))))), False) (@eq_ind_r Z Zvar3 (fun x : Z => forall _ : Z.le Z0 (Z.add (Z.add Zvar2 (Zneg xH)) (Z.opp x)), False) (fast_Zopp_eq_mult_neg_1 Zvar3 (fun x : Z => forall _ : Z.le Z0 (Z.add (Z.add Zvar2 (Zneg xH)) x), False) (fast_Zplus_comm (Z.add Zvar2 (Zneg xH)) (Z.mul Zvar3 (Zneg xH)) (fun x : Z => forall _ : Z.le Z0 x, False) (fast_Zred_factor0 Zvar2 (fun x : Z => forall _ : Z.le Z0 (Z.add (Z.mul Zvar3 (Zneg xH)) (Z.add x (Zneg xH))), False) (fun Omega12 : Z.le Z0 (Z.add (Z.mul Zvar3 (Zneg xH)) (Z.add (Z.mul Zvar2 (Zpos xH)) (Zneg xH))) => fast_OMEGA13 Zvar3 (Z.add (Z.mul Zvar2 (Zneg xH)) Z0) (Z.add (Z.mul Zvar2 (Zpos xH)) (Zneg xH)) xH (fun x : Z => forall _ : Z.le Z0 x, False) (fast_OMEGA14 Zvar2 Z0 (Zneg xH) xH (fun x : Z => forall _ : Z.le Z0 x, False) (fun H4 : not (@eq comparison Gt Gt) => False_ind False (H4 (@eq_refl comparison Gt)))) (OMEGA2 (Z.add (Z.mul Zvar3 (Zpos xH)) (Z.add (Z.mul Zvar2 (Zneg xH)) Z0)) (Z.add (Z.mul Zvar3 (Zneg xH)) (Z.add (Z.mul Zvar2 (Zpos xH)) (Zneg xH))) Omega14 Omega12))))) (Z.of_nat (Init.Nat.add n (@pos2nat n p))) Omega11) (Z.of_nat n) Omega9 (Zgt_left (Z.of_nat n) (Z.of_nat (Init.Nat.add n (@pos2nat n p))) (inj_gt n (Init.Nat.add n (@pos2nat n p)) Omega0)))))) (Z.of_nat n) Omega9) (Z.of_nat (Init.Nat.add n (@pos2nat n p))) Omega11 (Zle_left (Z.of_nat n) (Z.of_nat (Init.Nat.add n (@pos2nat n p))) (inj_le n (Init.Nat.add n (@pos2nat n p)) H1))) Omega15) (intro_Z (Init.Nat.add n (@pos2nat n p)))) Omega16) (intro_Z n)) (Z.of_nat (Init.Nat.sub (Init.Nat.add n (@pos2nat n p)) n)) (inj_minus2 (Init.Nat.add n (@pos2nat n p)) n Omega0)) (le_gt_dec n (Init.Nat.add n (@pos2nat n p))) (inj_ge (Init.Nat.sub (Init.Nat.add n (@pos2nat n p)) n) n (not_lt (Init.Nat.sub (Init.Nat.add n (@pos2nat n p)) n) n H))) (Z.of_nat (Init.Nat.mul (S (S O)) n)) (Nat2Z.inj_mul (S (S O)) n) (inj_lt (Init.Nat.add n (@pos2nat n p)) (Init.Nat.mul (S (S O)) n) H2))))) O end | right H1 => @eq (vec nat n) v (@vec_one n (@nat2pos n (Init.Nat.add n (@pos2nat n p)) H1)) end (@eq nat (@vec_pos nat n v p) O) *)
    destruct (le_lt_dec n (n+pos2nat p)); [ | omega ].
(* Goal: iff match le_lt_dec (Init.Nat.mul (S (S O)) n) (Init.Nat.add n (@pos2nat n p)) with | left l => @sss_compute (mm_instr n) (vec nat n) (@mm_sss n) P (@pair nat (vec nat n) (Init.Nat.sub (Init.Nat.add n (@pos2nat n p)) (Init.Nat.mul (S (S O)) n)) v) (@pair nat (vec nat n) k (@vec_zero n)) | right H2 => @eq nat (@vec_pos nat n v (@nat2pos n (Init.Nat.sub (Init.Nat.add n (@pos2nat n p)) n) (Decidable.dec_not_not (lt (Init.Nat.sub (Init.Nat.add n (@pos2nat n p)) n) n) (dec_lt (Init.Nat.sub (Init.Nat.add n (@pos2nat n p)) n) n) (fun H : not (lt (Init.Nat.sub (Init.Nat.add n (@pos2nat n p)) n) n) => @eq_ind_r Z (Z.mul (Z.of_nat (S (S O))) (Z.of_nat n)) (fun x : Z => forall _ : Z.lt (Z.of_nat (Init.Nat.add n (@pos2nat n p))) x, False) (fun H3 : Z.lt (Z.of_nat (Init.Nat.add n (@pos2nat n p))) (Z.mul (Zpos (xO xH)) (Z.of_nat n)) => @sumbool_ind (le n (Init.Nat.add n (@pos2nat n p))) (gt n (Init.Nat.add n (@pos2nat n p))) (fun _ : sumbool (le n (Init.Nat.add n (@pos2nat n p))) (gt n (Init.Nat.add n (@pos2nat n p))) => forall _ : Z.ge (Z.of_nat (Init.Nat.sub (Init.Nat.add n (@pos2nat n p)) n)) (Z.of_nat n), False) (fun Omega0 : le n (Init.Nat.add n (@pos2nat n p)) => @eq_ind_r Z (Z.sub (Z.of_nat (Init.Nat.add n (@pos2nat n p))) (Z.of_nat n)) (fun x : Z => forall _ : Z.ge x (Z.of_nat n), False) (fun H0 : Z.ge (Z.sub (Z.of_nat (Init.Nat.add n (@pos2nat n p))) (Z.of_nat n)) (Z.of_nat n) => @ex_ind Z (fun y : Z => and (@eq Z (Z.of_nat (Init.Nat.add n (@pos2nat n p))) y) (Z.le Z0 (Z.add (Z.mul y (Zpos xH)) Z0))) False (fun (Zvar0 : Z) (Omega8 : and (@eq Z (Z.of_nat (Init.Nat.add n (@pos2nat n p))) Zvar0) (Z.le Z0 (Z.add (Z.mul Zvar0 (Zpos xH)) Z0))) => @and_ind (@eq Z (Z.of_nat (Init.Nat.add n (@pos2nat n p))) Zvar0) (Z.le Z0 (Z.add (Z.mul Zvar0 (Zpos xH)) Z0)) False (fun (Omega1 : @eq Z (Z.of_nat (Init.Nat.add n (@pos2nat n p))) Zvar0) (_ : Z.le Z0 (Z.add (Z.mul Zvar0 (Zpos xH)) Z0)) => @ex_ind Z (fun y : Z => and (@eq Z (Z.of_nat n) y) (Z.le Z0 (Z.add (Z.mul y (Zpos xH)) Z0))) False (fun (Zvar1 : Z) (Omega7 : and (@eq Z (Z.of_nat n) Zvar1) (Z.le Z0 (Z.add (Z.mul Zvar1 (Zpos xH)) Z0))) => @and_ind (@eq Z (Z.of_nat n) Zvar1) (Z.le Z0 (Z.add (Z.mul Zvar1 (Zpos xH)) Z0)) False (fun (Omega2 : @eq Z (Z.of_nat n) Zvar1) (_ : Z.le Z0 (Z.add (Z.mul Zvar1 (Zpos xH)) Z0)) => @eq_ind_r Z Zvar1 (fun x : Z => forall _ : Z.le Z0 (Z.add (Z.add (Z.mul (Zpos (xO xH)) x) (Zneg xH)) (Z.opp (Z.of_nat (Init.Nat.add n (@pos2nat n p))))), False) (fast_Zmult_comm (Zpos (xO xH)) Zvar1 (fun x : Z => forall _ : Z.le Z0 (Z.add (Z.add x (Zneg xH)) (Z.opp (Z.of_nat (Init.Nat.add n (@pos2nat n p))))), False) (@eq_ind_r Z Zvar0 (fun x : Z => forall _ : Z.le Z0 (Z.add (Z.add (Z.mul Zvar1 (Zpos (xO xH))) (Zneg xH)) (Z.opp x)), False) (fast_Zopp_eq_mult_neg_1 Zvar0 (fun x : Z => forall _ : Z.le Z0 (Z.add (Z.add (Z.mul Zvar1 (Zpos (xO xH))) (Zneg xH)) x), False) (fast_Zplus_comm (Z.add (Z.mul Zvar1 (Zpos (xO xH))) (Zneg xH)) (Z.mul Zvar0 (Zneg xH)) (fun x : Z => forall _ : Z.le Z0 x, False) (fun Omega5 : Z.le Z0 (Z.add (Z.mul Zvar0 (Zneg xH)) (Z.add (Z.mul Zvar1 (Zpos (xO xH))) (Zneg xH))) => @eq_ind_r Z Zvar0 (fun x : Z => forall _ : Z.le Z0 (Z.add (Z.add x (Z.opp (Z.of_nat n))) (Z.opp (Z.of_nat n))), False) (@eq_ind_r Z Zvar1 (fun x : Z => forall _ : Z.le Z0 (Z.add (Z.add Zvar0 (Z.opp x)) (Z.opp (Z.of_nat n))), False) (fast_Zopp_eq_mult_neg_1 Zvar1 (fun x : Z => forall _ : Z.le Z0 (Z.add (Z.add Zvar0 x) (Z.opp (Z.of_nat n))), False) (@eq_ind_r Z Zvar1 (fun x : Z => forall _ : Z.le Z0 (Z.add (Z.add Zvar0 (Z.mul Zvar1 (Zneg xH))) (Z.opp x)), False) (fast_Zopp_eq_mult_neg_1 Zvar1 (fun x : Z => forall _ : Z.le Z0 (Z.add (Z.add Zvar0 (Z.mul Zvar1 (Zneg xH))) x), False) (fast_Zplus_assoc_reverse Zvar0 (Z.mul Zvar1 (Zneg xH)) (Z.mul Zvar1 (Zneg xH)) (fun x : Z => forall _ : Z.le Z0 x, False) (fast_Zred_factor0 Zvar0 (fun x : Z => forall _ : Z.le Z0 (Z.add x (Z.add (Z.mul Zvar1 (Zneg xH)) (Z.mul Zvar1 (Zneg xH)))), False) (fast_Zred_factor4 Zvar1 (Zneg xH) (Zneg xH) (fun x : Z => forall _ : Z.le Z0 (Z.add (Z.mul Zvar0 (Zpos xH)) x), False) (fast_Zred_factor6 (Z.mul Zvar1 (Zneg (xO xH))) (fun x : Z => forall _ : Z.le Z0 (Z.add (Z.mul Zvar0 (Zpos xH)) x), False) (fun Omega3 : Z.le Z0 (Z.add (Z.mul Zvar0 (Zpos xH)) (Z.add (Z.mul Zvar1 (Zneg (xO xH))) Z0)) => fast_OMEGA13 Zvar0 (Z.add (Z.mul Zvar1 (Zneg (xO xH))) Z0) (Z.add (Z.mul Zvar1 (Zpos (xO xH))) (Zneg xH)) xH (fun x : Z => forall _ : Z.le Z0 x, False) (fast_OMEGA14 Zvar1 Z0 (Zneg xH) (xO xH) (fun x : Z => forall _ : Z.le Z0 x, False) (fun H1 : not (@eq comparison Gt Gt) => False_ind False (H1 (@eq_refl comparison Gt)))) (OMEGA2 (Z.add (Z.mul Zvar0 (Zpos xH)) (Z.add (Z.mul Zvar1 (Zneg (xO xH))) Z0)) (Z.add (Z.mul Zvar0 (Zneg xH)) (Z.add (Z.mul Zvar1 (Zpos (xO xH))) (Zneg xH))) Omega3 Omega5))))))) (Z.of_nat n) Omega2)) (Z.of_nat n) Omega2) (Z.of_nat (Init.Nat.add n (@pos2nat n p))) Omega1 (Zge_left (Z.sub (Z.of_nat (Init.Nat.add n (@pos2nat n p))) (Z.of_nat n)) (Z.of_nat n) H0)))) (Z.of_nat (Init.Nat.add n (@pos2nat n p))) Omega1)) (Z.of_nat n) Omega2 (Zlt_left (Z.of_nat (Init.Nat.add n (@pos2nat n p))) (Z.mul (Zpos (xO xH)) (Z.of_nat n)) H3)) Omega7) (intro_Z n)) Omega8) (intro_Z (Init.Nat.add n (@pos2nat n p)))) (Z.of_nat (Init.Nat.sub (Init.Nat.add n (@pos2nat n p)) n)) (Nat2Z.inj_sub (Init.Nat.add n (@pos2nat n p)) n Omega0)) (fun Omega0 : gt n (Init.Nat.add n (@pos2nat n p)) => @eq_ind_r Z Z0 (fun x : Z => forall _ : Z.ge x (Z.of_nat n), False) (fun _ : Z.ge Z0 (Z.of_nat n) => @ex_ind Z (fun y : Z => and (@eq Z (Z.of_nat n) y) (Z.le Z0 (Z.add (Z.mul y (Zpos xH)) Z0))) False (fun (Zvar2 : Z) (Omega16 : and (@eq Z (Z.of_nat n) Zvar2) (Z.le Z0 (Z.add (Z.mul Zvar2 (Zpos xH)) Z0))) => @and_ind (@eq Z (Z.of_nat n) Zvar2) (Z.le Z0 (Z.add (Z.mul Zvar2 (Zpos xH)) Z0)) False (fun (Omega9 : @eq Z (Z.of_nat n) Zvar2) (_ : Z.le Z0 (Z.add (Z.mul Zvar2 (Zpos xH)) Z0)) => @ex_ind Z (fun y : Z => and (@eq Z (Z.of_nat (Init.Nat.add n (@pos2nat n p))) y) (Z.le Z0 (Z.add (Z.mul y (Zpos xH)) Z0))) False (fun (Zvar3 : Z) (Omega15 : and (@eq Z (Z.of_nat (Init.Nat.add n (@pos2nat n p))) Zvar3) (Z.le Z0 (Z.add (Z.mul Zvar3 (Zpos xH)) Z0))) => @and_ind (@eq Z (Z.of_nat (Init.Nat.add n (@pos2nat n p))) Zvar3) (Z.le Z0 (Z.add (Z.mul Zvar3 (Zpos xH)) Z0)) False (fun (Omega11 : @eq Z (Z.of_nat (Init.Nat.add n (@pos2nat n p))) Zvar3) (_ : Z.le Z0 (Z.add (Z.mul Zvar3 (Zpos xH)) Z0)) => @eq_ind_r Z Zvar3 (fun x : Z => forall _ : Z.le Z0 (Z.add x (Z.opp (Z.of_nat n))), False) (@eq_ind_r Z Zvar2 (fun x : Z => forall _ : Z.le Z0 (Z.add Zvar3 (Z.opp x)), False) (fast_Zopp_eq_mult_neg_1 Zvar2 (fun x : Z => forall _ : Z.le Z0 (Z.add Zvar3 x), False) (fast_Zred_factor0 Zvar3 (fun x : Z => forall _ : Z.le Z0 (Z.add x (Z.mul Zvar2 (Zneg xH))), False) (fast_Zred_factor6 (Z.mul Zvar2 (Zneg xH)) (fun x : Z => forall _ : Z.le Z0 (Z.add (Z.mul Zvar3 (Zpos xH)) x), False) (fun Omega14 : Z.le Z0 (Z.add (Z.mul Zvar3 (Zpos xH)) (Z.add (Z.mul Zvar2 (Zneg xH)) Z0)) => @eq_ind_r Z Zvar2 (fun x : Z => forall _ : Z.le Z0 (Z.add (Z.add x (Zneg xH)) (Z.opp (Z.of_nat (Init.Nat.add n (@pos2nat n p))))), False) (@eq_ind_r Z Zvar3 (fun x : Z => forall _ : Z.le Z0 (Z.add (Z.add Zvar2 (Zneg xH)) (Z.opp x)), False) (fast_Zopp_eq_mult_neg_1 Zvar3 (fun x : Z => forall _ : Z.le Z0 (Z.add (Z.add Zvar2 (Zneg xH)) x), False) (fast_Zplus_comm (Z.add Zvar2 (Zneg xH)) (Z.mul Zvar3 (Zneg xH)) (fun x : Z => forall _ : Z.le Z0 x, False) (fast_Zred_factor0 Zvar2 (fun x : Z => forall _ : Z.le Z0 (Z.add (Z.mul Zvar3 (Zneg xH)) (Z.add x (Zneg xH))), False) (fun Omega12 : Z.le Z0 (Z.add (Z.mul Zvar3 (Zneg xH)) (Z.add (Z.mul Zvar2 (Zpos xH)) (Zneg xH))) => fast_OMEGA13 Zvar3 (Z.add (Z.mul Zvar2 (Zneg xH)) Z0) (Z.add (Z.mul Zvar2 (Zpos xH)) (Zneg xH)) xH (fun x : Z => forall _ : Z.le Z0 x, False) (fast_OMEGA14 Zvar2 Z0 (Zneg xH) xH (fun x : Z => forall _ : Z.le Z0 x, False) (fun H1 : not (@eq comparison Gt Gt) => False_ind False (H1 (@eq_refl comparison Gt)))) (OMEGA2 (Z.add (Z.mul Zvar3 (Zpos xH)) (Z.add (Z.mul Zvar2 (Zneg xH)) Z0)) (Z.add (Z.mul Zvar3 (Zneg xH)) (Z.add (Z.mul Zvar2 (Zpos xH)) (Zneg xH))) Omega14 Omega12))))) (Z.of_nat (Init.Nat.add n (@pos2nat n p))) Omega11) (Z.of_nat n) Omega9 (Zgt_left (Z.of_nat n) (Z.of_nat (Init.Nat.add n (@pos2nat n p))) (inj_gt n (Init.Nat.add n (@pos2nat n p)) Omega0)))))) (Z.of_nat n) Omega9) (Z.of_nat (Init.Nat.add n (@pos2nat n p))) Omega11 (Zle_left (Z.of_nat n) (Z.of_nat (Init.Nat.add n (@pos2nat n p))) (inj_le n (Init.Nat.add n (@pos2nat n p)) l))) Omega15) (intro_Z (Init.Nat.add n (@pos2nat n p)))) Omega16) (intro_Z n)) (Z.of_nat (Init.Nat.sub (Init.Nat.add n (@pos2nat n p)) n)) (inj_minus2 (Init.Nat.add n (@pos2nat n p)) n Omega0)) (le_gt_dec n (Init.Nat.add n (@pos2nat n p))) (inj_ge (Init.Nat.sub (Init.Nat.add n (@pos2nat n p)) n) n (not_lt (Init.Nat.sub (Init.Nat.add n (@pos2nat n p)) n) n H))) (Z.of_nat (Init.Nat.mul (S (S O)) n)) (Nat2Z.inj_mul (S (S O)) n) (inj_lt (Init.Nat.add n (@pos2nat n p)) (Init.Nat.mul (S (S O)) n) H2))))) O end (@eq nat (@vec_pos nat n v p) O) *)
    destruct (le_lt_dec (2*n) (n+pos2nat p)).
(* Goal: iff (@sss_compute (mm_instr n) (vec nat n) (@mm_sss n) P (@pair nat (vec nat n) (Init.Nat.sub (Init.Nat.add n (@pos2nat n p)) (Init.Nat.mul (S (S O)) n)) v) (@pair nat (vec nat n) k (@vec_zero n))) (@eq nat (@vec_pos nat n v p) O) *)
(* Goal: iff (@eq nat (@vec_pos nat n v (@nat2pos n (Init.Nat.sub (Init.Nat.add n (@pos2nat n p)) n) (Decidable.dec_not_not (lt (Init.Nat.sub (Init.Nat.add n (@pos2nat n p)) n) n) (dec_lt (Init.Nat.sub (Init.Nat.add n (@pos2nat n p)) n) n) (fun H : not (lt (Init.Nat.sub (Init.Nat.add n (@pos2nat n p)) n) n) => @eq_ind_r Z (Z.mul (Z.of_nat (S (S O))) (Z.of_nat n)) (fun x : Z => forall _ : Z.lt (Z.of_nat (Init.Nat.add n (@pos2nat n p))) x, False) (fun H2 : Z.lt (Z.of_nat (Init.Nat.add n (@pos2nat n p))) (Z.mul (Zpos (xO xH)) (Z.of_nat n)) => @sumbool_ind (le n (Init.Nat.add n (@pos2nat n p))) (gt n (Init.Nat.add n (@pos2nat n p))) (fun _ : sumbool (le n (Init.Nat.add n (@pos2nat n p))) (gt n (Init.Nat.add n (@pos2nat n p))) => forall _ : Z.ge (Z.of_nat (Init.Nat.sub (Init.Nat.add n (@pos2nat n p)) n)) (Z.of_nat n), False) (fun Omega0 : le n (Init.Nat.add n (@pos2nat n p)) => @eq_ind_r Z (Z.sub (Z.of_nat (Init.Nat.add n (@pos2nat n p))) (Z.of_nat n)) (fun x : Z => forall _ : Z.ge x (Z.of_nat n), False) (fun H0 : Z.ge (Z.sub (Z.of_nat (Init.Nat.add n (@pos2nat n p))) (Z.of_nat n)) (Z.of_nat n) => @ex_ind Z (fun y : Z => and (@eq Z (Z.of_nat (Init.Nat.add n (@pos2nat n p))) y) (Z.le Z0 (Z.add (Z.mul y (Zpos xH)) Z0))) False (fun (Zvar0 : Z) (Omega8 : and (@eq Z (Z.of_nat (Init.Nat.add n (@pos2nat n p))) Zvar0) (Z.le Z0 (Z.add (Z.mul Zvar0 (Zpos xH)) Z0))) => @and_ind (@eq Z (Z.of_nat (Init.Nat.add n (@pos2nat n p))) Zvar0) (Z.le Z0 (Z.add (Z.mul Zvar0 (Zpos xH)) Z0)) False (fun (Omega1 : @eq Z (Z.of_nat (Init.Nat.add n (@pos2nat n p))) Zvar0) (_ : Z.le Z0 (Z.add (Z.mul Zvar0 (Zpos xH)) Z0)) => @ex_ind Z (fun y : Z => and (@eq Z (Z.of_nat n) y) (Z.le Z0 (Z.add (Z.mul y (Zpos xH)) Z0))) False (fun (Zvar1 : Z) (Omega7 : and (@eq Z (Z.of_nat n) Zvar1) (Z.le Z0 (Z.add (Z.mul Zvar1 (Zpos xH)) Z0))) => @and_ind (@eq Z (Z.of_nat n) Zvar1) (Z.le Z0 (Z.add (Z.mul Zvar1 (Zpos xH)) Z0)) False (fun (Omega2 : @eq Z (Z.of_nat n) Zvar1) (_ : Z.le Z0 (Z.add (Z.mul Zvar1 (Zpos xH)) Z0)) => @eq_ind_r Z Zvar1 (fun x : Z => forall _ : Z.le Z0 (Z.add (Z.add (Z.mul (Zpos (xO xH)) x) (Zneg xH)) (Z.opp (Z.of_nat (Init.Nat.add n (@pos2nat n p))))), False) (fast_Zmult_comm (Zpos (xO xH)) Zvar1 (fun x : Z => forall _ : Z.le Z0 (Z.add (Z.add x (Zneg xH)) (Z.opp (Z.of_nat (Init.Nat.add n (@pos2nat n p))))), False) (@eq_ind_r Z Zvar0 (fun x : Z => forall _ : Z.le Z0 (Z.add (Z.add (Z.mul Zvar1 (Zpos (xO xH))) (Zneg xH)) (Z.opp x)), False) (fast_Zopp_eq_mult_neg_1 Zvar0 (fun x : Z => forall _ : Z.le Z0 (Z.add (Z.add (Z.mul Zvar1 (Zpos (xO xH))) (Zneg xH)) x), False) (fast_Zplus_comm (Z.add (Z.mul Zvar1 (Zpos (xO xH))) (Zneg xH)) (Z.mul Zvar0 (Zneg xH)) (fun x : Z => forall _ : Z.le Z0 x, False) (fun Omega5 : Z.le Z0 (Z.add (Z.mul Zvar0 (Zneg xH)) (Z.add (Z.mul Zvar1 (Zpos (xO xH))) (Zneg xH))) => @eq_ind_r Z Zvar0 (fun x : Z => forall _ : Z.le Z0 (Z.add (Z.add x (Z.opp (Z.of_nat n))) (Z.opp (Z.of_nat n))), False) (@eq_ind_r Z Zvar1 (fun x : Z => forall _ : Z.le Z0 (Z.add (Z.add Zvar0 (Z.opp x)) (Z.opp (Z.of_nat n))), False) (fast_Zopp_eq_mult_neg_1 Zvar1 (fun x : Z => forall _ : Z.le Z0 (Z.add (Z.add Zvar0 x) (Z.opp (Z.of_nat n))), False) (@eq_ind_r Z Zvar1 (fun x : Z => forall _ : Z.le Z0 (Z.add (Z.add Zvar0 (Z.mul Zvar1 (Zneg xH))) (Z.opp x)), False) (fast_Zopp_eq_mult_neg_1 Zvar1 (fun x : Z => forall _ : Z.le Z0 (Z.add (Z.add Zvar0 (Z.mul Zvar1 (Zneg xH))) x), False) (fast_Zplus_assoc_reverse Zvar0 (Z.mul Zvar1 (Zneg xH)) (Z.mul Zvar1 (Zneg xH)) (fun x : Z => forall _ : Z.le Z0 x, False) (fast_Zred_factor0 Zvar0 (fun x : Z => forall _ : Z.le Z0 (Z.add x (Z.add (Z.mul Zvar1 (Zneg xH)) (Z.mul Zvar1 (Zneg xH)))), False) (fast_Zred_factor4 Zvar1 (Zneg xH) (Zneg xH) (fun x : Z => forall _ : Z.le Z0 (Z.add (Z.mul Zvar0 (Zpos xH)) x), False) (fast_Zred_factor6 (Z.mul Zvar1 (Zneg (xO xH))) (fun x : Z => forall _ : Z.le Z0 (Z.add (Z.mul Zvar0 (Zpos xH)) x), False) (fun Omega3 : Z.le Z0 (Z.add (Z.mul Zvar0 (Zpos xH)) (Z.add (Z.mul Zvar1 (Zneg (xO xH))) Z0)) => fast_OMEGA13 Zvar0 (Z.add (Z.mul Zvar1 (Zneg (xO xH))) Z0) (Z.add (Z.mul Zvar1 (Zpos (xO xH))) (Zneg xH)) xH (fun x : Z => forall _ : Z.le Z0 x, False) (fast_OMEGA14 Zvar1 Z0 (Zneg xH) (xO xH) (fun x : Z => forall _ : Z.le Z0 x, False) (fun H1 : not (@eq comparison Gt Gt) => False_ind False (H1 (@eq_refl comparison Gt)))) (OMEGA2 (Z.add (Z.mul Zvar0 (Zpos xH)) (Z.add (Z.mul Zvar1 (Zneg (xO xH))) Z0)) (Z.add (Z.mul Zvar0 (Zneg xH)) (Z.add (Z.mul Zvar1 (Zpos (xO xH))) (Zneg xH))) Omega3 Omega5))))))) (Z.of_nat n) Omega2)) (Z.of_nat n) Omega2) (Z.of_nat (Init.Nat.add n (@pos2nat n p))) Omega1 (Zge_left (Z.sub (Z.of_nat (Init.Nat.add n (@pos2nat n p))) (Z.of_nat n)) (Z.of_nat n) H0)))) (Z.of_nat (Init.Nat.add n (@pos2nat n p))) Omega1)) (Z.of_nat n) Omega2 (Zlt_left (Z.of_nat (Init.Nat.add n (@pos2nat n p))) (Z.mul (Zpos (xO xH)) (Z.of_nat n)) H2)) Omega7) (intro_Z n)) Omega8) (intro_Z (Init.Nat.add n (@pos2nat n p)))) (Z.of_nat (Init.Nat.sub (Init.Nat.add n (@pos2nat n p)) n)) (Nat2Z.inj_sub (Init.Nat.add n (@pos2nat n p)) n Omega0)) (fun Omega0 : gt n (Init.Nat.add n (@pos2nat n p)) => @eq_ind_r Z Z0 (fun x : Z => forall _ : Z.ge x (Z.of_nat n), False) (fun _ : Z.ge Z0 (Z.of_nat n) => @ex_ind Z (fun y : Z => and (@eq Z (Z.of_nat n) y) (Z.le Z0 (Z.add (Z.mul y (Zpos xH)) Z0))) False (fun (Zvar2 : Z) (Omega16 : and (@eq Z (Z.of_nat n) Zvar2) (Z.le Z0 (Z.add (Z.mul Zvar2 (Zpos xH)) Z0))) => @and_ind (@eq Z (Z.of_nat n) Zvar2) (Z.le Z0 (Z.add (Z.mul Zvar2 (Zpos xH)) Z0)) False (fun (Omega9 : @eq Z (Z.of_nat n) Zvar2) (_ : Z.le Z0 (Z.add (Z.mul Zvar2 (Zpos xH)) Z0)) => @ex_ind Z (fun y : Z => and (@eq Z (Z.of_nat (Init.Nat.add n (@pos2nat n p))) y) (Z.le Z0 (Z.add (Z.mul y (Zpos xH)) Z0))) False (fun (Zvar3 : Z) (Omega15 : and (@eq Z (Z.of_nat (Init.Nat.add n (@pos2nat n p))) Zvar3) (Z.le Z0 (Z.add (Z.mul Zvar3 (Zpos xH)) Z0))) => @and_ind (@eq Z (Z.of_nat (Init.Nat.add n (@pos2nat n p))) Zvar3) (Z.le Z0 (Z.add (Z.mul Zvar3 (Zpos xH)) Z0)) False (fun (Omega11 : @eq Z (Z.of_nat (Init.Nat.add n (@pos2nat n p))) Zvar3) (_ : Z.le Z0 (Z.add (Z.mul Zvar3 (Zpos xH)) Z0)) => @eq_ind_r Z Zvar3 (fun x : Z => forall _ : Z.le Z0 (Z.add x (Z.opp (Z.of_nat n))), False) (@eq_ind_r Z Zvar2 (fun x : Z => forall _ : Z.le Z0 (Z.add Zvar3 (Z.opp x)), False) (fast_Zopp_eq_mult_neg_1 Zvar2 (fun x : Z => forall _ : Z.le Z0 (Z.add Zvar3 x), False) (fast_Zred_factor0 Zvar3 (fun x : Z => forall _ : Z.le Z0 (Z.add x (Z.mul Zvar2 (Zneg xH))), False) (fast_Zred_factor6 (Z.mul Zvar2 (Zneg xH)) (fun x : Z => forall _ : Z.le Z0 (Z.add (Z.mul Zvar3 (Zpos xH)) x), False) (fun Omega14 : Z.le Z0 (Z.add (Z.mul Zvar3 (Zpos xH)) (Z.add (Z.mul Zvar2 (Zneg xH)) Z0)) => @eq_ind_r Z Zvar2 (fun x : Z => forall _ : Z.le Z0 (Z.add (Z.add x (Zneg xH)) (Z.opp (Z.of_nat (Init.Nat.add n (@pos2nat n p))))), False) (@eq_ind_r Z Zvar3 (fun x : Z => forall _ : Z.le Z0 (Z.add (Z.add Zvar2 (Zneg xH)) (Z.opp x)), False) (fast_Zopp_eq_mult_neg_1 Zvar3 (fun x : Z => forall _ : Z.le Z0 (Z.add (Z.add Zvar2 (Zneg xH)) x), False) (fast_Zplus_comm (Z.add Zvar2 (Zneg xH)) (Z.mul Zvar3 (Zneg xH)) (fun x : Z => forall _ : Z.le Z0 x, False) (fast_Zred_factor0 Zvar2 (fun x : Z => forall _ : Z.le Z0 (Z.add (Z.mul Zvar3 (Zneg xH)) (Z.add x (Zneg xH))), False) (fun Omega12 : Z.le Z0 (Z.add (Z.mul Zvar3 (Zneg xH)) (Z.add (Z.mul Zvar2 (Zpos xH)) (Zneg xH))) => fast_OMEGA13 Zvar3 (Z.add (Z.mul Zvar2 (Zneg xH)) Z0) (Z.add (Z.mul Zvar2 (Zpos xH)) (Zneg xH)) xH (fun x : Z => forall _ : Z.le Z0 x, False) (fast_OMEGA14 Zvar2 Z0 (Zneg xH) xH (fun x : Z => forall _ : Z.le Z0 x, False) (fun H1 : not (@eq comparison Gt Gt) => False_ind False (H1 (@eq_refl comparison Gt)))) (OMEGA2 (Z.add (Z.mul Zvar3 (Zpos xH)) (Z.add (Z.mul Zvar2 (Zneg xH)) Z0)) (Z.add (Z.mul Zvar3 (Zneg xH)) (Z.add (Z.mul Zvar2 (Zpos xH)) (Zneg xH))) Omega14 Omega12))))) (Z.of_nat (Init.Nat.add n (@pos2nat n p))) Omega11) (Z.of_nat n) Omega9 (Zgt_left (Z.of_nat n) (Z.of_nat (Init.Nat.add n (@pos2nat n p))) (inj_gt n (Init.Nat.add n (@pos2nat n p)) Omega0)))))) (Z.of_nat n) Omega9) (Z.of_nat (Init.Nat.add n (@pos2nat n p))) Omega11 (Zle_left (Z.of_nat n) (Z.of_nat (Init.Nat.add n (@pos2nat n p))) (inj_le n (Init.Nat.add n (@pos2nat n p)) l))) Omega15) (intro_Z (Init.Nat.add n (@pos2nat n p)))) Omega16) (intro_Z n)) (Z.of_nat (Init.Nat.sub (Init.Nat.add n (@pos2nat n p)) n)) (inj_minus2 (Init.Nat.add n (@pos2nat n p)) n Omega0)) (le_gt_dec n (Init.Nat.add n (@pos2nat n p))) (inj_ge (Init.Nat.sub (Init.Nat.add n (@pos2nat n p)) n) n (not_lt (Init.Nat.sub (Init.Nat.add n (@pos2nat n p)) n) n H))) (Z.of_nat (Init.Nat.mul (S (S O)) n)) (Nat2Z.inj_mul (S (S O)) n) (inj_lt (Init.Nat.add n (@pos2nat n p)) (Init.Nat.mul (S (S O)) n) l0))))) O) (@eq nat (@vec_pos nat n v p) O) *)
    generalize (pos2nat_prop p); omega.
(* Goal: iff (@eq nat (@vec_pos nat n v (@nat2pos n (Init.Nat.sub (Init.Nat.add n (@pos2nat n p)) n) (Decidable.dec_not_not (lt (Init.Nat.sub (Init.Nat.add n (@pos2nat n p)) n) n) (dec_lt (Init.Nat.sub (Init.Nat.add n (@pos2nat n p)) n) n) (fun H : not (lt (Init.Nat.sub (Init.Nat.add n (@pos2nat n p)) n) n) => @eq_ind_r Z (Z.mul (Z.of_nat (S (S O))) (Z.of_nat n)) (fun x : Z => forall _ : Z.lt (Z.of_nat (Init.Nat.add n (@pos2nat n p))) x, False) (fun H2 : Z.lt (Z.of_nat (Init.Nat.add n (@pos2nat n p))) (Z.mul (Zpos (xO xH)) (Z.of_nat n)) => @sumbool_ind (le n (Init.Nat.add n (@pos2nat n p))) (gt n (Init.Nat.add n (@pos2nat n p))) (fun _ : sumbool (le n (Init.Nat.add n (@pos2nat n p))) (gt n (Init.Nat.add n (@pos2nat n p))) => forall _ : Z.ge (Z.of_nat (Init.Nat.sub (Init.Nat.add n (@pos2nat n p)) n)) (Z.of_nat n), False) (fun Omega0 : le n (Init.Nat.add n (@pos2nat n p)) => @eq_ind_r Z (Z.sub (Z.of_nat (Init.Nat.add n (@pos2nat n p))) (Z.of_nat n)) (fun x : Z => forall _ : Z.ge x (Z.of_nat n), False) (fun H0 : Z.ge (Z.sub (Z.of_nat (Init.Nat.add n (@pos2nat n p))) (Z.of_nat n)) (Z.of_nat n) => @ex_ind Z (fun y : Z => and (@eq Z (Z.of_nat (Init.Nat.add n (@pos2nat n p))) y) (Z.le Z0 (Z.add (Z.mul y (Zpos xH)) Z0))) False (fun (Zvar0 : Z) (Omega8 : and (@eq Z (Z.of_nat (Init.Nat.add n (@pos2nat n p))) Zvar0) (Z.le Z0 (Z.add (Z.mul Zvar0 (Zpos xH)) Z0))) => @and_ind (@eq Z (Z.of_nat (Init.Nat.add n (@pos2nat n p))) Zvar0) (Z.le Z0 (Z.add (Z.mul Zvar0 (Zpos xH)) Z0)) False (fun (Omega1 : @eq Z (Z.of_nat (Init.Nat.add n (@pos2nat n p))) Zvar0) (_ : Z.le Z0 (Z.add (Z.mul Zvar0 (Zpos xH)) Z0)) => @ex_ind Z (fun y : Z => and (@eq Z (Z.of_nat n) y) (Z.le Z0 (Z.add (Z.mul y (Zpos xH)) Z0))) False (fun (Zvar1 : Z) (Omega7 : and (@eq Z (Z.of_nat n) Zvar1) (Z.le Z0 (Z.add (Z.mul Zvar1 (Zpos xH)) Z0))) => @and_ind (@eq Z (Z.of_nat n) Zvar1) (Z.le Z0 (Z.add (Z.mul Zvar1 (Zpos xH)) Z0)) False (fun (Omega2 : @eq Z (Z.of_nat n) Zvar1) (_ : Z.le Z0 (Z.add (Z.mul Zvar1 (Zpos xH)) Z0)) => @eq_ind_r Z Zvar1 (fun x : Z => forall _ : Z.le Z0 (Z.add (Z.add (Z.mul (Zpos (xO xH)) x) (Zneg xH)) (Z.opp (Z.of_nat (Init.Nat.add n (@pos2nat n p))))), False) (fast_Zmult_comm (Zpos (xO xH)) Zvar1 (fun x : Z => forall _ : Z.le Z0 (Z.add (Z.add x (Zneg xH)) (Z.opp (Z.of_nat (Init.Nat.add n (@pos2nat n p))))), False) (@eq_ind_r Z Zvar0 (fun x : Z => forall _ : Z.le Z0 (Z.add (Z.add (Z.mul Zvar1 (Zpos (xO xH))) (Zneg xH)) (Z.opp x)), False) (fast_Zopp_eq_mult_neg_1 Zvar0 (fun x : Z => forall _ : Z.le Z0 (Z.add (Z.add (Z.mul Zvar1 (Zpos (xO xH))) (Zneg xH)) x), False) (fast_Zplus_comm (Z.add (Z.mul Zvar1 (Zpos (xO xH))) (Zneg xH)) (Z.mul Zvar0 (Zneg xH)) (fun x : Z => forall _ : Z.le Z0 x, False) (fun Omega5 : Z.le Z0 (Z.add (Z.mul Zvar0 (Zneg xH)) (Z.add (Z.mul Zvar1 (Zpos (xO xH))) (Zneg xH))) => @eq_ind_r Z Zvar0 (fun x : Z => forall _ : Z.le Z0 (Z.add (Z.add x (Z.opp (Z.of_nat n))) (Z.opp (Z.of_nat n))), False) (@eq_ind_r Z Zvar1 (fun x : Z => forall _ : Z.le Z0 (Z.add (Z.add Zvar0 (Z.opp x)) (Z.opp (Z.of_nat n))), False) (fast_Zopp_eq_mult_neg_1 Zvar1 (fun x : Z => forall _ : Z.le Z0 (Z.add (Z.add Zvar0 x) (Z.opp (Z.of_nat n))), False) (@eq_ind_r Z Zvar1 (fun x : Z => forall _ : Z.le Z0 (Z.add (Z.add Zvar0 (Z.mul Zvar1 (Zneg xH))) (Z.opp x)), False) (fast_Zopp_eq_mult_neg_1 Zvar1 (fun x : Z => forall _ : Z.le Z0 (Z.add (Z.add Zvar0 (Z.mul Zvar1 (Zneg xH))) x), False) (fast_Zplus_assoc_reverse Zvar0 (Z.mul Zvar1 (Zneg xH)) (Z.mul Zvar1 (Zneg xH)) (fun x : Z => forall _ : Z.le Z0 x, False) (fast_Zred_factor0 Zvar0 (fun x : Z => forall _ : Z.le Z0 (Z.add x (Z.add (Z.mul Zvar1 (Zneg xH)) (Z.mul Zvar1 (Zneg xH)))), False) (fast_Zred_factor4 Zvar1 (Zneg xH) (Zneg xH) (fun x : Z => forall _ : Z.le Z0 (Z.add (Z.mul Zvar0 (Zpos xH)) x), False) (fast_Zred_factor6 (Z.mul Zvar1 (Zneg (xO xH))) (fun x : Z => forall _ : Z.le Z0 (Z.add (Z.mul Zvar0 (Zpos xH)) x), False) (fun Omega3 : Z.le Z0 (Z.add (Z.mul Zvar0 (Zpos xH)) (Z.add (Z.mul Zvar1 (Zneg (xO xH))) Z0)) => fast_OMEGA13 Zvar0 (Z.add (Z.mul Zvar1 (Zneg (xO xH))) Z0) (Z.add (Z.mul Zvar1 (Zpos (xO xH))) (Zneg xH)) xH (fun x : Z => forall _ : Z.le Z0 x, False) (fast_OMEGA14 Zvar1 Z0 (Zneg xH) (xO xH) (fun x : Z => forall _ : Z.le Z0 x, False) (fun H1 : not (@eq comparison Gt Gt) => False_ind False (H1 (@eq_refl comparison Gt)))) (OMEGA2 (Z.add (Z.mul Zvar0 (Zpos xH)) (Z.add (Z.mul Zvar1 (Zneg (xO xH))) Z0)) (Z.add (Z.mul Zvar0 (Zneg xH)) (Z.add (Z.mul Zvar1 (Zpos (xO xH))) (Zneg xH))) Omega3 Omega5))))))) (Z.of_nat n) Omega2)) (Z.of_nat n) Omega2) (Z.of_nat (Init.Nat.add n (@pos2nat n p))) Omega1 (Zge_left (Z.sub (Z.of_nat (Init.Nat.add n (@pos2nat n p))) (Z.of_nat n)) (Z.of_nat n) H0)))) (Z.of_nat (Init.Nat.add n (@pos2nat n p))) Omega1)) (Z.of_nat n) Omega2 (Zlt_left (Z.of_nat (Init.Nat.add n (@pos2nat n p))) (Z.mul (Zpos (xO xH)) (Z.of_nat n)) H2)) Omega7) (intro_Z n)) Omega8) (intro_Z (Init.Nat.add n (@pos2nat n p)))) (Z.of_nat (Init.Nat.sub (Init.Nat.add n (@pos2nat n p)) n)) (Nat2Z.inj_sub (Init.Nat.add n (@pos2nat n p)) n Omega0)) (fun Omega0 : gt n (Init.Nat.add n (@pos2nat n p)) => @eq_ind_r Z Z0 (fun x : Z => forall _ : Z.ge x (Z.of_nat n), False) (fun _ : Z.ge Z0 (Z.of_nat n) => @ex_ind Z (fun y : Z => and (@eq Z (Z.of_nat n) y) (Z.le Z0 (Z.add (Z.mul y (Zpos xH)) Z0))) False (fun (Zvar2 : Z) (Omega16 : and (@eq Z (Z.of_nat n) Zvar2) (Z.le Z0 (Z.add (Z.mul Zvar2 (Zpos xH)) Z0))) => @and_ind (@eq Z (Z.of_nat n) Zvar2) (Z.le Z0 (Z.add (Z.mul Zvar2 (Zpos xH)) Z0)) False (fun (Omega9 : @eq Z (Z.of_nat n) Zvar2) (_ : Z.le Z0 (Z.add (Z.mul Zvar2 (Zpos xH)) Z0)) => @ex_ind Z (fun y : Z => and (@eq Z (Z.of_nat (Init.Nat.add n (@pos2nat n p))) y) (Z.le Z0 (Z.add (Z.mul y (Zpos xH)) Z0))) False (fun (Zvar3 : Z) (Omega15 : and (@eq Z (Z.of_nat (Init.Nat.add n (@pos2nat n p))) Zvar3) (Z.le Z0 (Z.add (Z.mul Zvar3 (Zpos xH)) Z0))) => @and_ind (@eq Z (Z.of_nat (Init.Nat.add n (@pos2nat n p))) Zvar3) (Z.le Z0 (Z.add (Z.mul Zvar3 (Zpos xH)) Z0)) False (fun (Omega11 : @eq Z (Z.of_nat (Init.Nat.add n (@pos2nat n p))) Zvar3) (_ : Z.le Z0 (Z.add (Z.mul Zvar3 (Zpos xH)) Z0)) => @eq_ind_r Z Zvar3 (fun x : Z => forall _ : Z.le Z0 (Z.add x (Z.opp (Z.of_nat n))), False) (@eq_ind_r Z Zvar2 (fun x : Z => forall _ : Z.le Z0 (Z.add Zvar3 (Z.opp x)), False) (fast_Zopp_eq_mult_neg_1 Zvar2 (fun x : Z => forall _ : Z.le Z0 (Z.add Zvar3 x), False) (fast_Zred_factor0 Zvar3 (fun x : Z => forall _ : Z.le Z0 (Z.add x (Z.mul Zvar2 (Zneg xH))), False) (fast_Zred_factor6 (Z.mul Zvar2 (Zneg xH)) (fun x : Z => forall _ : Z.le Z0 (Z.add (Z.mul Zvar3 (Zpos xH)) x), False) (fun Omega14 : Z.le Z0 (Z.add (Z.mul Zvar3 (Zpos xH)) (Z.add (Z.mul Zvar2 (Zneg xH)) Z0)) => @eq_ind_r Z Zvar2 (fun x : Z => forall _ : Z.le Z0 (Z.add (Z.add x (Zneg xH)) (Z.opp (Z.of_nat (Init.Nat.add n (@pos2nat n p))))), False) (@eq_ind_r Z Zvar3 (fun x : Z => forall _ : Z.le Z0 (Z.add (Z.add Zvar2 (Zneg xH)) (Z.opp x)), False) (fast_Zopp_eq_mult_neg_1 Zvar3 (fun x : Z => forall _ : Z.le Z0 (Z.add (Z.add Zvar2 (Zneg xH)) x), False) (fast_Zplus_comm (Z.add Zvar2 (Zneg xH)) (Z.mul Zvar3 (Zneg xH)) (fun x : Z => forall _ : Z.le Z0 x, False) (fast_Zred_factor0 Zvar2 (fun x : Z => forall _ : Z.le Z0 (Z.add (Z.mul Zvar3 (Zneg xH)) (Z.add x (Zneg xH))), False) (fun Omega12 : Z.le Z0 (Z.add (Z.mul Zvar3 (Zneg xH)) (Z.add (Z.mul Zvar2 (Zpos xH)) (Zneg xH))) => fast_OMEGA13 Zvar3 (Z.add (Z.mul Zvar2 (Zneg xH)) Z0) (Z.add (Z.mul Zvar2 (Zpos xH)) (Zneg xH)) xH (fun x : Z => forall _ : Z.le Z0 x, False) (fast_OMEGA14 Zvar2 Z0 (Zneg xH) xH (fun x : Z => forall _ : Z.le Z0 x, False) (fun H1 : not (@eq comparison Gt Gt) => False_ind False (H1 (@eq_refl comparison Gt)))) (OMEGA2 (Z.add (Z.mul Zvar3 (Zpos xH)) (Z.add (Z.mul Zvar2 (Zneg xH)) Z0)) (Z.add (Z.mul Zvar3 (Zneg xH)) (Z.add (Z.mul Zvar2 (Zpos xH)) (Zneg xH))) Omega14 Omega12))))) (Z.of_nat (Init.Nat.add n (@pos2nat n p))) Omega11) (Z.of_nat n) Omega9 (Zgt_left (Z.of_nat n) (Z.of_nat (Init.Nat.add n (@pos2nat n p))) (inj_gt n (Init.Nat.add n (@pos2nat n p)) Omega0)))))) (Z.of_nat n) Omega9) (Z.of_nat (Init.Nat.add n (@pos2nat n p))) Omega11 (Zle_left (Z.of_nat n) (Z.of_nat (Init.Nat.add n (@pos2nat n p))) (inj_le n (Init.Nat.add n (@pos2nat n p)) l))) Omega15) (intro_Z (Init.Nat.add n (@pos2nat n p)))) Omega16) (intro_Z n)) (Z.of_nat (Init.Nat.sub (Init.Nat.add n (@pos2nat n p)) n)) (inj_minus2 (Init.Nat.add n (@pos2nat n p)) n Omega0)) (le_gt_dec n (Init.Nat.add n (@pos2nat n p))) (inj_ge (Init.Nat.sub (Init.Nat.add n (@pos2nat n p)) n) n (not_lt (Init.Nat.sub (Init.Nat.add n (@pos2nat n p)) n) n H))) (Z.of_nat (Init.Nat.mul (S (S O)) n)) (Nat2Z.inj_mul (S (S O)) n) (inj_lt (Init.Nat.add n (@pos2nat n p)) (Init.Nat.mul (S (S O)) n) l0))))) O) (@eq nat (@vec_pos nat n v p) O) *)
    match goal with |- vec_pos _ (nat2pos ?H) = _ <-> _ => cutrewrite (nat2pos H = p) end.
(* Goal: iff (@eq nat (@vec_pos nat n v p) O) (@eq nat (@vec_pos nat n v p) O) *)
(* Goal: @eq (pos n) (@nat2pos n (Init.Nat.sub (Init.Nat.add n (@pos2nat n p)) n) (Decidable.dec_not_not (lt (Init.Nat.sub (Init.Nat.add n (@pos2nat n p)) n) n) (dec_lt (Init.Nat.sub (Init.Nat.add n (@pos2nat n p)) n) n) (fun H : not (lt (Init.Nat.sub (Init.Nat.add n (@pos2nat n p)) n) n) => @eq_ind_r Z (Z.mul (Z.of_nat (S (S O))) (Z.of_nat n)) (fun x : Z => forall _ : Z.lt (Z.of_nat (Init.Nat.add n (@pos2nat n p))) x, False) (fun H2 : Z.lt (Z.of_nat (Init.Nat.add n (@pos2nat n p))) (Z.mul (Zpos (xO xH)) (Z.of_nat n)) => @sumbool_ind (le n (Init.Nat.add n (@pos2nat n p))) (gt n (Init.Nat.add n (@pos2nat n p))) (fun _ : sumbool (le n (Init.Nat.add n (@pos2nat n p))) (gt n (Init.Nat.add n (@pos2nat n p))) => forall _ : Z.ge (Z.of_nat (Init.Nat.sub (Init.Nat.add n (@pos2nat n p)) n)) (Z.of_nat n), False) (fun Omega0 : le n (Init.Nat.add n (@pos2nat n p)) => @eq_ind_r Z (Z.sub (Z.of_nat (Init.Nat.add n (@pos2nat n p))) (Z.of_nat n)) (fun x : Z => forall _ : Z.ge x (Z.of_nat n), False) (fun H0 : Z.ge (Z.sub (Z.of_nat (Init.Nat.add n (@pos2nat n p))) (Z.of_nat n)) (Z.of_nat n) => @ex_ind Z (fun y : Z => and (@eq Z (Z.of_nat (Init.Nat.add n (@pos2nat n p))) y) (Z.le Z0 (Z.add (Z.mul y (Zpos xH)) Z0))) False (fun (Zvar0 : Z) (Omega8 : and (@eq Z (Z.of_nat (Init.Nat.add n (@pos2nat n p))) Zvar0) (Z.le Z0 (Z.add (Z.mul Zvar0 (Zpos xH)) Z0))) => @and_ind (@eq Z (Z.of_nat (Init.Nat.add n (@pos2nat n p))) Zvar0) (Z.le Z0 (Z.add (Z.mul Zvar0 (Zpos xH)) Z0)) False (fun (Omega1 : @eq Z (Z.of_nat (Init.Nat.add n (@pos2nat n p))) Zvar0) (_ : Z.le Z0 (Z.add (Z.mul Zvar0 (Zpos xH)) Z0)) => @ex_ind Z (fun y : Z => and (@eq Z (Z.of_nat n) y) (Z.le Z0 (Z.add (Z.mul y (Zpos xH)) Z0))) False (fun (Zvar1 : Z) (Omega7 : and (@eq Z (Z.of_nat n) Zvar1) (Z.le Z0 (Z.add (Z.mul Zvar1 (Zpos xH)) Z0))) => @and_ind (@eq Z (Z.of_nat n) Zvar1) (Z.le Z0 (Z.add (Z.mul Zvar1 (Zpos xH)) Z0)) False (fun (Omega2 : @eq Z (Z.of_nat n) Zvar1) (_ : Z.le Z0 (Z.add (Z.mul Zvar1 (Zpos xH)) Z0)) => @eq_ind_r Z Zvar1 (fun x : Z => forall _ : Z.le Z0 (Z.add (Z.add (Z.mul (Zpos (xO xH)) x) (Zneg xH)) (Z.opp (Z.of_nat (Init.Nat.add n (@pos2nat n p))))), False) (fast_Zmult_comm (Zpos (xO xH)) Zvar1 (fun x : Z => forall _ : Z.le Z0 (Z.add (Z.add x (Zneg xH)) (Z.opp (Z.of_nat (Init.Nat.add n (@pos2nat n p))))), False) (@eq_ind_r Z Zvar0 (fun x : Z => forall _ : Z.le Z0 (Z.add (Z.add (Z.mul Zvar1 (Zpos (xO xH))) (Zneg xH)) (Z.opp x)), False) (fast_Zopp_eq_mult_neg_1 Zvar0 (fun x : Z => forall _ : Z.le Z0 (Z.add (Z.add (Z.mul Zvar1 (Zpos (xO xH))) (Zneg xH)) x), False) (fast_Zplus_comm (Z.add (Z.mul Zvar1 (Zpos (xO xH))) (Zneg xH)) (Z.mul Zvar0 (Zneg xH)) (fun x : Z => forall _ : Z.le Z0 x, False) (fun Omega5 : Z.le Z0 (Z.add (Z.mul Zvar0 (Zneg xH)) (Z.add (Z.mul Zvar1 (Zpos (xO xH))) (Zneg xH))) => @eq_ind_r Z Zvar0 (fun x : Z => forall _ : Z.le Z0 (Z.add (Z.add x (Z.opp (Z.of_nat n))) (Z.opp (Z.of_nat n))), False) (@eq_ind_r Z Zvar1 (fun x : Z => forall _ : Z.le Z0 (Z.add (Z.add Zvar0 (Z.opp x)) (Z.opp (Z.of_nat n))), False) (fast_Zopp_eq_mult_neg_1 Zvar1 (fun x : Z => forall _ : Z.le Z0 (Z.add (Z.add Zvar0 x) (Z.opp (Z.of_nat n))), False) (@eq_ind_r Z Zvar1 (fun x : Z => forall _ : Z.le Z0 (Z.add (Z.add Zvar0 (Z.mul Zvar1 (Zneg xH))) (Z.opp x)), False) (fast_Zopp_eq_mult_neg_1 Zvar1 (fun x : Z => forall _ : Z.le Z0 (Z.add (Z.add Zvar0 (Z.mul Zvar1 (Zneg xH))) x), False) (fast_Zplus_assoc_reverse Zvar0 (Z.mul Zvar1 (Zneg xH)) (Z.mul Zvar1 (Zneg xH)) (fun x : Z => forall _ : Z.le Z0 x, False) (fast_Zred_factor0 Zvar0 (fun x : Z => forall _ : Z.le Z0 (Z.add x (Z.add (Z.mul Zvar1 (Zneg xH)) (Z.mul Zvar1 (Zneg xH)))), False) (fast_Zred_factor4 Zvar1 (Zneg xH) (Zneg xH) (fun x : Z => forall _ : Z.le Z0 (Z.add (Z.mul Zvar0 (Zpos xH)) x), False) (fast_Zred_factor6 (Z.mul Zvar1 (Zneg (xO xH))) (fun x : Z => forall _ : Z.le Z0 (Z.add (Z.mul Zvar0 (Zpos xH)) x), False) (fun Omega3 : Z.le Z0 (Z.add (Z.mul Zvar0 (Zpos xH)) (Z.add (Z.mul Zvar1 (Zneg (xO xH))) Z0)) => fast_OMEGA13 Zvar0 (Z.add (Z.mul Zvar1 (Zneg (xO xH))) Z0) (Z.add (Z.mul Zvar1 (Zpos (xO xH))) (Zneg xH)) xH (fun x : Z => forall _ : Z.le Z0 x, False) (fast_OMEGA14 Zvar1 Z0 (Zneg xH) (xO xH) (fun x : Z => forall _ : Z.le Z0 x, False) (fun H1 : not (@eq comparison Gt Gt) => False_ind False (H1 (@eq_refl comparison Gt)))) (OMEGA2 (Z.add (Z.mul Zvar0 (Zpos xH)) (Z.add (Z.mul Zvar1 (Zneg (xO xH))) Z0)) (Z.add (Z.mul Zvar0 (Zneg xH)) (Z.add (Z.mul Zvar1 (Zpos (xO xH))) (Zneg xH))) Omega3 Omega5))))))) (Z.of_nat n) Omega2)) (Z.of_nat n) Omega2) (Z.of_nat (Init.Nat.add n (@pos2nat n p))) Omega1 (Zge_left (Z.sub (Z.of_nat (Init.Nat.add n (@pos2nat n p))) (Z.of_nat n)) (Z.of_nat n) H0)))) (Z.of_nat (Init.Nat.add n (@pos2nat n p))) Omega1)) (Z.of_nat n) Omega2 (Zlt_left (Z.of_nat (Init.Nat.add n (@pos2nat n p))) (Z.mul (Zpos (xO xH)) (Z.of_nat n)) H2)) Omega7) (intro_Z n)) Omega8) (intro_Z (Init.Nat.add n (@pos2nat n p)))) (Z.of_nat (Init.Nat.sub (Init.Nat.add n (@pos2nat n p)) n)) (Nat2Z.inj_sub (Init.Nat.add n (@pos2nat n p)) n Omega0)) (fun Omega0 : gt n (Init.Nat.add n (@pos2nat n p)) => @eq_ind_r Z Z0 (fun x : Z => forall _ : Z.ge x (Z.of_nat n), False) (fun _ : Z.ge Z0 (Z.of_nat n) => @ex_ind Z (fun y : Z => and (@eq Z (Z.of_nat n) y) (Z.le Z0 (Z.add (Z.mul y (Zpos xH)) Z0))) False (fun (Zvar2 : Z) (Omega16 : and (@eq Z (Z.of_nat n) Zvar2) (Z.le Z0 (Z.add (Z.mul Zvar2 (Zpos xH)) Z0))) => @and_ind (@eq Z (Z.of_nat n) Zvar2) (Z.le Z0 (Z.add (Z.mul Zvar2 (Zpos xH)) Z0)) False (fun (Omega9 : @eq Z (Z.of_nat n) Zvar2) (_ : Z.le Z0 (Z.add (Z.mul Zvar2 (Zpos xH)) Z0)) => @ex_ind Z (fun y : Z => and (@eq Z (Z.of_nat (Init.Nat.add n (@pos2nat n p))) y) (Z.le Z0 (Z.add (Z.mul y (Zpos xH)) Z0))) False (fun (Zvar3 : Z) (Omega15 : and (@eq Z (Z.of_nat (Init.Nat.add n (@pos2nat n p))) Zvar3) (Z.le Z0 (Z.add (Z.mul Zvar3 (Zpos xH)) Z0))) => @and_ind (@eq Z (Z.of_nat (Init.Nat.add n (@pos2nat n p))) Zvar3) (Z.le Z0 (Z.add (Z.mul Zvar3 (Zpos xH)) Z0)) False (fun (Omega11 : @eq Z (Z.of_nat (Init.Nat.add n (@pos2nat n p))) Zvar3) (_ : Z.le Z0 (Z.add (Z.mul Zvar3 (Zpos xH)) Z0)) => @eq_ind_r Z Zvar3 (fun x : Z => forall _ : Z.le Z0 (Z.add x (Z.opp (Z.of_nat n))), False) (@eq_ind_r Z Zvar2 (fun x : Z => forall _ : Z.le Z0 (Z.add Zvar3 (Z.opp x)), False) (fast_Zopp_eq_mult_neg_1 Zvar2 (fun x : Z => forall _ : Z.le Z0 (Z.add Zvar3 x), False) (fast_Zred_factor0 Zvar3 (fun x : Z => forall _ : Z.le Z0 (Z.add x (Z.mul Zvar2 (Zneg xH))), False) (fast_Zred_factor6 (Z.mul Zvar2 (Zneg xH)) (fun x : Z => forall _ : Z.le Z0 (Z.add (Z.mul Zvar3 (Zpos xH)) x), False) (fun Omega14 : Z.le Z0 (Z.add (Z.mul Zvar3 (Zpos xH)) (Z.add (Z.mul Zvar2 (Zneg xH)) Z0)) => @eq_ind_r Z Zvar2 (fun x : Z => forall _ : Z.le Z0 (Z.add (Z.add x (Zneg xH)) (Z.opp (Z.of_nat (Init.Nat.add n (@pos2nat n p))))), False) (@eq_ind_r Z Zvar3 (fun x : Z => forall _ : Z.le Z0 (Z.add (Z.add Zvar2 (Zneg xH)) (Z.opp x)), False) (fast_Zopp_eq_mult_neg_1 Zvar3 (fun x : Z => forall _ : Z.le Z0 (Z.add (Z.add Zvar2 (Zneg xH)) x), False) (fast_Zplus_comm (Z.add Zvar2 (Zneg xH)) (Z.mul Zvar3 (Zneg xH)) (fun x : Z => forall _ : Z.le Z0 x, False) (fast_Zred_factor0 Zvar2 (fun x : Z => forall _ : Z.le Z0 (Z.add (Z.mul Zvar3 (Zneg xH)) (Z.add x (Zneg xH))), False) (fun Omega12 : Z.le Z0 (Z.add (Z.mul Zvar3 (Zneg xH)) (Z.add (Z.mul Zvar2 (Zpos xH)) (Zneg xH))) => fast_OMEGA13 Zvar3 (Z.add (Z.mul Zvar2 (Zneg xH)) Z0) (Z.add (Z.mul Zvar2 (Zpos xH)) (Zneg xH)) xH (fun x : Z => forall _ : Z.le Z0 x, False) (fast_OMEGA14 Zvar2 Z0 (Zneg xH) xH (fun x : Z => forall _ : Z.le Z0 x, False) (fun H1 : not (@eq comparison Gt Gt) => False_ind False (H1 (@eq_refl comparison Gt)))) (OMEGA2 (Z.add (Z.mul Zvar3 (Zpos xH)) (Z.add (Z.mul Zvar2 (Zneg xH)) Z0)) (Z.add (Z.mul Zvar3 (Zneg xH)) (Z.add (Z.mul Zvar2 (Zpos xH)) (Zneg xH))) Omega14 Omega12))))) (Z.of_nat (Init.Nat.add n (@pos2nat n p))) Omega11) (Z.of_nat n) Omega9 (Zgt_left (Z.of_nat n) (Z.of_nat (Init.Nat.add n (@pos2nat n p))) (inj_gt n (Init.Nat.add n (@pos2nat n p)) Omega0)))))) (Z.of_nat n) Omega9) (Z.of_nat (Init.Nat.add n (@pos2nat n p))) Omega11 (Zle_left (Z.of_nat n) (Z.of_nat (Init.Nat.add n (@pos2nat n p))) (inj_le n (Init.Nat.add n (@pos2nat n p)) l))) Omega15) (intro_Z (Init.Nat.add n (@pos2nat n p)))) Omega16) (intro_Z n)) (Z.of_nat (Init.Nat.sub (Init.Nat.add n (@pos2nat n p)) n)) (inj_minus2 (Init.Nat.add n (@pos2nat n p)) n Omega0)) (le_gt_dec n (Init.Nat.add n (@pos2nat n p))) (inj_ge (Init.Nat.sub (Init.Nat.add n (@pos2nat n p)) n) n (not_lt (Init.Nat.sub (Init.Nat.add n (@pos2nat n p)) n) n H))) (Z.of_nat (Init.Nat.mul (S (S O)) n)) (Nat2Z.inj_mul (S (S O)) n) (inj_lt (Init.Nat.add n (@pos2nat n p)) (Init.Nat.mul (S (S O)) n) l0)))) p *)
    tauto.
(* Goal: @eq (pos n) (@nat2pos n (Init.Nat.sub (Init.Nat.add n (@pos2nat n p)) n) (Decidable.dec_not_not (lt (Init.Nat.sub (Init.Nat.add n (@pos2nat n p)) n) n) (dec_lt (Init.Nat.sub (Init.Nat.add n (@pos2nat n p)) n) n) (fun H : not (lt (Init.Nat.sub (Init.Nat.add n (@pos2nat n p)) n) n) => @eq_ind_r Z (Z.mul (Z.of_nat (S (S O))) (Z.of_nat n)) (fun x : Z => forall _ : Z.lt (Z.of_nat (Init.Nat.add n (@pos2nat n p))) x, False) (fun H2 : Z.lt (Z.of_nat (Init.Nat.add n (@pos2nat n p))) (Z.mul (Zpos (xO xH)) (Z.of_nat n)) => @sumbool_ind (le n (Init.Nat.add n (@pos2nat n p))) (gt n (Init.Nat.add n (@pos2nat n p))) (fun _ : sumbool (le n (Init.Nat.add n (@pos2nat n p))) (gt n (Init.Nat.add n (@pos2nat n p))) => forall _ : Z.ge (Z.of_nat (Init.Nat.sub (Init.Nat.add n (@pos2nat n p)) n)) (Z.of_nat n), False) (fun Omega0 : le n (Init.Nat.add n (@pos2nat n p)) => @eq_ind_r Z (Z.sub (Z.of_nat (Init.Nat.add n (@pos2nat n p))) (Z.of_nat n)) (fun x : Z => forall _ : Z.ge x (Z.of_nat n), False) (fun H0 : Z.ge (Z.sub (Z.of_nat (Init.Nat.add n (@pos2nat n p))) (Z.of_nat n)) (Z.of_nat n) => @ex_ind Z (fun y : Z => and (@eq Z (Z.of_nat (Init.Nat.add n (@pos2nat n p))) y) (Z.le Z0 (Z.add (Z.mul y (Zpos xH)) Z0))) False (fun (Zvar0 : Z) (Omega8 : and (@eq Z (Z.of_nat (Init.Nat.add n (@pos2nat n p))) Zvar0) (Z.le Z0 (Z.add (Z.mul Zvar0 (Zpos xH)) Z0))) => @and_ind (@eq Z (Z.of_nat (Init.Nat.add n (@pos2nat n p))) Zvar0) (Z.le Z0 (Z.add (Z.mul Zvar0 (Zpos xH)) Z0)) False (fun (Omega1 : @eq Z (Z.of_nat (Init.Nat.add n (@pos2nat n p))) Zvar0) (_ : Z.le Z0 (Z.add (Z.mul Zvar0 (Zpos xH)) Z0)) => @ex_ind Z (fun y : Z => and (@eq Z (Z.of_nat n) y) (Z.le Z0 (Z.add (Z.mul y (Zpos xH)) Z0))) False (fun (Zvar1 : Z) (Omega7 : and (@eq Z (Z.of_nat n) Zvar1) (Z.le Z0 (Z.add (Z.mul Zvar1 (Zpos xH)) Z0))) => @and_ind (@eq Z (Z.of_nat n) Zvar1) (Z.le Z0 (Z.add (Z.mul Zvar1 (Zpos xH)) Z0)) False (fun (Omega2 : @eq Z (Z.of_nat n) Zvar1) (_ : Z.le Z0 (Z.add (Z.mul Zvar1 (Zpos xH)) Z0)) => @eq_ind_r Z Zvar1 (fun x : Z => forall _ : Z.le Z0 (Z.add (Z.add (Z.mul (Zpos (xO xH)) x) (Zneg xH)) (Z.opp (Z.of_nat (Init.Nat.add n (@pos2nat n p))))), False) (fast_Zmult_comm (Zpos (xO xH)) Zvar1 (fun x : Z => forall _ : Z.le Z0 (Z.add (Z.add x (Zneg xH)) (Z.opp (Z.of_nat (Init.Nat.add n (@pos2nat n p))))), False) (@eq_ind_r Z Zvar0 (fun x : Z => forall _ : Z.le Z0 (Z.add (Z.add (Z.mul Zvar1 (Zpos (xO xH))) (Zneg xH)) (Z.opp x)), False) (fast_Zopp_eq_mult_neg_1 Zvar0 (fun x : Z => forall _ : Z.le Z0 (Z.add (Z.add (Z.mul Zvar1 (Zpos (xO xH))) (Zneg xH)) x), False) (fast_Zplus_comm (Z.add (Z.mul Zvar1 (Zpos (xO xH))) (Zneg xH)) (Z.mul Zvar0 (Zneg xH)) (fun x : Z => forall _ : Z.le Z0 x, False) (fun Omega5 : Z.le Z0 (Z.add (Z.mul Zvar0 (Zneg xH)) (Z.add (Z.mul Zvar1 (Zpos (xO xH))) (Zneg xH))) => @eq_ind_r Z Zvar0 (fun x : Z => forall _ : Z.le Z0 (Z.add (Z.add x (Z.opp (Z.of_nat n))) (Z.opp (Z.of_nat n))), False) (@eq_ind_r Z Zvar1 (fun x : Z => forall _ : Z.le Z0 (Z.add (Z.add Zvar0 (Z.opp x)) (Z.opp (Z.of_nat n))), False) (fast_Zopp_eq_mult_neg_1 Zvar1 (fun x : Z => forall _ : Z.le Z0 (Z.add (Z.add Zvar0 x) (Z.opp (Z.of_nat n))), False) (@eq_ind_r Z Zvar1 (fun x : Z => forall _ : Z.le Z0 (Z.add (Z.add Zvar0 (Z.mul Zvar1 (Zneg xH))) (Z.opp x)), False) (fast_Zopp_eq_mult_neg_1 Zvar1 (fun x : Z => forall _ : Z.le Z0 (Z.add (Z.add Zvar0 (Z.mul Zvar1 (Zneg xH))) x), False) (fast_Zplus_assoc_reverse Zvar0 (Z.mul Zvar1 (Zneg xH)) (Z.mul Zvar1 (Zneg xH)) (fun x : Z => forall _ : Z.le Z0 x, False) (fast_Zred_factor0 Zvar0 (fun x : Z => forall _ : Z.le Z0 (Z.add x (Z.add (Z.mul Zvar1 (Zneg xH)) (Z.mul Zvar1 (Zneg xH)))), False) (fast_Zred_factor4 Zvar1 (Zneg xH) (Zneg xH) (fun x : Z => forall _ : Z.le Z0 (Z.add (Z.mul Zvar0 (Zpos xH)) x), False) (fast_Zred_factor6 (Z.mul Zvar1 (Zneg (xO xH))) (fun x : Z => forall _ : Z.le Z0 (Z.add (Z.mul Zvar0 (Zpos xH)) x), False) (fun Omega3 : Z.le Z0 (Z.add (Z.mul Zvar0 (Zpos xH)) (Z.add (Z.mul Zvar1 (Zneg (xO xH))) Z0)) => fast_OMEGA13 Zvar0 (Z.add (Z.mul Zvar1 (Zneg (xO xH))) Z0) (Z.add (Z.mul Zvar1 (Zpos (xO xH))) (Zneg xH)) xH (fun x : Z => forall _ : Z.le Z0 x, False) (fast_OMEGA14 Zvar1 Z0 (Zneg xH) (xO xH) (fun x : Z => forall _ : Z.le Z0 x, False) (fun H1 : not (@eq comparison Gt Gt) => False_ind False (H1 (@eq_refl comparison Gt)))) (OMEGA2 (Z.add (Z.mul Zvar0 (Zpos xH)) (Z.add (Z.mul Zvar1 (Zneg (xO xH))) Z0)) (Z.add (Z.mul Zvar0 (Zneg xH)) (Z.add (Z.mul Zvar1 (Zpos (xO xH))) (Zneg xH))) Omega3 Omega5))))))) (Z.of_nat n) Omega2)) (Z.of_nat n) Omega2) (Z.of_nat (Init.Nat.add n (@pos2nat n p))) Omega1 (Zge_left (Z.sub (Z.of_nat (Init.Nat.add n (@pos2nat n p))) (Z.of_nat n)) (Z.of_nat n) H0)))) (Z.of_nat (Init.Nat.add n (@pos2nat n p))) Omega1)) (Z.of_nat n) Omega2 (Zlt_left (Z.of_nat (Init.Nat.add n (@pos2nat n p))) (Z.mul (Zpos (xO xH)) (Z.of_nat n)) H2)) Omega7) (intro_Z n)) Omega8) (intro_Z (Init.Nat.add n (@pos2nat n p)))) (Z.of_nat (Init.Nat.sub (Init.Nat.add n (@pos2nat n p)) n)) (Nat2Z.inj_sub (Init.Nat.add n (@pos2nat n p)) n Omega0)) (fun Omega0 : gt n (Init.Nat.add n (@pos2nat n p)) => @eq_ind_r Z Z0 (fun x : Z => forall _ : Z.ge x (Z.of_nat n), False) (fun _ : Z.ge Z0 (Z.of_nat n) => @ex_ind Z (fun y : Z => and (@eq Z (Z.of_nat n) y) (Z.le Z0 (Z.add (Z.mul y (Zpos xH)) Z0))) False (fun (Zvar2 : Z) (Omega16 : and (@eq Z (Z.of_nat n) Zvar2) (Z.le Z0 (Z.add (Z.mul Zvar2 (Zpos xH)) Z0))) => @and_ind (@eq Z (Z.of_nat n) Zvar2) (Z.le Z0 (Z.add (Z.mul Zvar2 (Zpos xH)) Z0)) False (fun (Omega9 : @eq Z (Z.of_nat n) Zvar2) (_ : Z.le Z0 (Z.add (Z.mul Zvar2 (Zpos xH)) Z0)) => @ex_ind Z (fun y : Z => and (@eq Z (Z.of_nat (Init.Nat.add n (@pos2nat n p))) y) (Z.le Z0 (Z.add (Z.mul y (Zpos xH)) Z0))) False (fun (Zvar3 : Z) (Omega15 : and (@eq Z (Z.of_nat (Init.Nat.add n (@pos2nat n p))) Zvar3) (Z.le Z0 (Z.add (Z.mul Zvar3 (Zpos xH)) Z0))) => @and_ind (@eq Z (Z.of_nat (Init.Nat.add n (@pos2nat n p))) Zvar3) (Z.le Z0 (Z.add (Z.mul Zvar3 (Zpos xH)) Z0)) False (fun (Omega11 : @eq Z (Z.of_nat (Init.Nat.add n (@pos2nat n p))) Zvar3) (_ : Z.le Z0 (Z.add (Z.mul Zvar3 (Zpos xH)) Z0)) => @eq_ind_r Z Zvar3 (fun x : Z => forall _ : Z.le Z0 (Z.add x (Z.opp (Z.of_nat n))), False) (@eq_ind_r Z Zvar2 (fun x : Z => forall _ : Z.le Z0 (Z.add Zvar3 (Z.opp x)), False) (fast_Zopp_eq_mult_neg_1 Zvar2 (fun x : Z => forall _ : Z.le Z0 (Z.add Zvar3 x), False) (fast_Zred_factor0 Zvar3 (fun x : Z => forall _ : Z.le Z0 (Z.add x (Z.mul Zvar2 (Zneg xH))), False) (fast_Zred_factor6 (Z.mul Zvar2 (Zneg xH)) (fun x : Z => forall _ : Z.le Z0 (Z.add (Z.mul Zvar3 (Zpos xH)) x), False) (fun Omega14 : Z.le Z0 (Z.add (Z.mul Zvar3 (Zpos xH)) (Z.add (Z.mul Zvar2 (Zneg xH)) Z0)) => @eq_ind_r Z Zvar2 (fun x : Z => forall _ : Z.le Z0 (Z.add (Z.add x (Zneg xH)) (Z.opp (Z.of_nat (Init.Nat.add n (@pos2nat n p))))), False) (@eq_ind_r Z Zvar3 (fun x : Z => forall _ : Z.le Z0 (Z.add (Z.add Zvar2 (Zneg xH)) (Z.opp x)), False) (fast_Zopp_eq_mult_neg_1 Zvar3 (fun x : Z => forall _ : Z.le Z0 (Z.add (Z.add Zvar2 (Zneg xH)) x), False) (fast_Zplus_comm (Z.add Zvar2 (Zneg xH)) (Z.mul Zvar3 (Zneg xH)) (fun x : Z => forall _ : Z.le Z0 x, False) (fast_Zred_factor0 Zvar2 (fun x : Z => forall _ : Z.le Z0 (Z.add (Z.mul Zvar3 (Zneg xH)) (Z.add x (Zneg xH))), False) (fun Omega12 : Z.le Z0 (Z.add (Z.mul Zvar3 (Zneg xH)) (Z.add (Z.mul Zvar2 (Zpos xH)) (Zneg xH))) => fast_OMEGA13 Zvar3 (Z.add (Z.mul Zvar2 (Zneg xH)) Z0) (Z.add (Z.mul Zvar2 (Zpos xH)) (Zneg xH)) xH (fun x : Z => forall _ : Z.le Z0 x, False) (fast_OMEGA14 Zvar2 Z0 (Zneg xH) xH (fun x : Z => forall _ : Z.le Z0 x, False) (fun H1 : not (@eq comparison Gt Gt) => False_ind False (H1 (@eq_refl comparison Gt)))) (OMEGA2 (Z.add (Z.mul Zvar3 (Zpos xH)) (Z.add (Z.mul Zvar2 (Zneg xH)) Z0)) (Z.add (Z.mul Zvar3 (Zneg xH)) (Z.add (Z.mul Zvar2 (Zpos xH)) (Zneg xH))) Omega14 Omega12))))) (Z.of_nat (Init.Nat.add n (@pos2nat n p))) Omega11) (Z.of_nat n) Omega9 (Zgt_left (Z.of_nat n) (Z.of_nat (Init.Nat.add n (@pos2nat n p))) (inj_gt n (Init.Nat.add n (@pos2nat n p)) Omega0)))))) (Z.of_nat n) Omega9) (Z.of_nat (Init.Nat.add n (@pos2nat n p))) Omega11 (Zle_left (Z.of_nat n) (Z.of_nat (Init.Nat.add n (@pos2nat n p))) (inj_le n (Init.Nat.add n (@pos2nat n p)) l))) Omega15) (intro_Z (Init.Nat.add n (@pos2nat n p)))) Omega16) (intro_Z n)) (Z.of_nat (Init.Nat.sub (Init.Nat.add n (@pos2nat n p)) n)) (inj_minus2 (Init.Nat.add n (@pos2nat n p)) n Omega0)) (le_gt_dec n (Init.Nat.add n (@pos2nat n p))) (inj_ge (Init.Nat.sub (Init.Nat.add n (@pos2nat n p)) n) n (not_lt (Init.Nat.sub (Init.Nat.add n (@pos2nat n p)) n) n H))) (Z.of_nat (Init.Nat.mul (S (S O)) n)) (Nat2Z.inj_mul (S (S O)) n) (inj_lt (Init.Nat.add n (@pos2nat n p)) (Init.Nat.mul (S (S O)) n) l0)))) p *)
    apply pos2nat_inj; rewrite pos2nat_nat2pos; omega.
  Qed.

  (* No need of the code of s anymore *)

  Opaque s.

  (* This is a notation for the trivial phase semantics *)
 
  Notation "'[[' A ']]'" := (ll_tps s A) (at level 65).

  (* i -o (_j_ -o _j_) *)
  
  Let sem_x_y_y i j : i <> j -> [[ [i LL_DEC (rx i) (ry j) (ry j) ] ]] vec_zero.
  Proof.
(* Goal: forall _ : not (@eq (pos n) i j), @ll_tps n s (eill_cmd_map (in_ll_cmd_dec (rx i) (ry j) (ry j))) (@vec_zero n) *)
    intros Hij.
(* Goal: @ll_tps n s (eill_cmd_map (in_ll_cmd_dec (rx x) (q (Init.Nat.add (S O) j)) (q j))) (@vec_zero n) *)
    simpl; unfold ll_tps_imp.
(* Goal: forall (x0 : vec nat n) (_ : forall (x1 : vec nat n) (_ : s (rx x) x1), s (q (S j)) (@vec_plus n x1 x0)), s (q j) (@vec_plus n x0 (@vec_zero n)) *)
(* Goal: @ll_tps n s (eill_cmd_map (in_ll_cmd_fork (ry x) (q p) (q j))) (@vec_zero n) *)
(* Goal: @ll_tps n s (eill_cmd_map (in_ll_cmd_dec (rx x) (q (Init.Nat.add (S O) j)) (q j))) (@vec_zero n) *)
    intros v Hv.
(* Goal: forall (x : vec nat n) (_ : s (ry j) x), s (ry j) (@vec_plus n x (@vec_plus n v (@vec_zero n))) *)
    rewrite H_s_rx in Hv.
(* Goal: forall (x : vec nat n) (_ : s (ry j) x), s (ry j) (@vec_plus n x (@vec_plus n v (@vec_zero n))) *)
    intros w Hw.
(* Goal: s (ry j) (@vec_plus n w (@vec_plus n v (@vec_zero n))) *)
    rewrite H_s_ry in Hw.
(* Goal: s (ry j) (@vec_plus n w (@vec_plus n v (@vec_zero n))) *)
    rewrite H_s_ry.
(* Goal: s (q j) (@vec_plus n w (@vec_plus n v (@vec_zero n))) *)
    rewrite (vec_plus_comm v), vec_zero_plus.
(* Goal: @eq nat (@vec_pos nat n (@vec_plus n w v) j) O *)
    unfold vec_plus; rewrite vec_pos_set.
(* Goal: @eq nat (Init.Nat.add (@vec_pos nat n w j) (@vec_pos nat n v j)) O *)
    subst; rewrite Hw, vec_one_spec_neq; auto.
  Qed.
  
  Let sem_y_y_y j : [[ [i LL_INC (ry j) (ry j) (ry j) ] ]] vec_zero.
  Proof.
(* Goal: @ll_tps n s (eill_cmd_map (in_ll_cmd_dec (rx x) (q (Init.Nat.add (S O) j)) (q j))) (@vec_zero n) *)
    simpl; unfold ll_tps_imp.
(* Goal: forall (x : vec nat n) (_ : forall (x0 : vec nat n) (_ : s (q k) x0), s (q k) (@vec_plus n x0 x)), s (q k) (@vec_plus n x (@vec_zero n)) *)
    intros x Hx; rew vec.
(* Goal: s (q k) x *)
    generalize (Hx vec_zero); rew vec.
(* Goal: forall _ : forall _ : s (ry j) (@vec_zero n), s (ry j) x, s (ry j) x *)
    intros H; apply H, H_s_ry; rew vec.
  Qed.
 
  (* We need out_code k P here *)
  
  Let sem_k v : [[£ (q k)]] v <-> v = vec_zero.
  Proof.
    simpl; rewrite H_s_q.
(* Goal: iff (@sss_compute (mm_instr n) (vec nat n) (@mm_sss n) P (@pair nat (vec nat n) i v) (@pair nat (vec nat n) k (@vec_zero n))) (G_eill Sig (@vec_map_list nat n v rx) (q i)) *)
    split.
    2: intros; subst; exists 0; constructor. 
(* Goal: forall _ : @eq nat (@vec_pos nat n v p) O, G_eill Sig (@app nat (@vec_map_list nat n v rx) (@nil nat)) (ry p) *)
    intros H.
    apply sss_compute_stop in H; auto.
    inversion H; auto.
  Qed.
  
  Let sem_k_k_k : [[ [i LL_INC (q k) (q k) (q k) ] ]] vec_zero.
  Proof.
(* Goal: @ll_tps n s (eill_cmd_map (in_ll_cmd_dec (rx x) (q (Init.Nat.add (S O) j)) (q j))) (@vec_zero n) *)
    simpl; unfold ll_tps_imp.
(* Goal: forall (x : vec nat n) (_ : forall (x0 : vec nat n) (_ : s (q k) x0), s (q k) (@vec_plus n x0 x)), s (q k) (@vec_plus n x (@vec_zero n)) *)
    intros x Hx; rew vec.
(* Goal: s (q k) x *)
    generalize (Hx vec_zero); rew vec.
(* Goal: forall _ : forall _ : s (q k) (@vec_zero n), s (q k) x, s (q k) x *)
    intros H; apply H, sem_k; auto.
  Qed.

  Let Sig0_zero A : In A Sig0 -> [[ [iA] ]] vec_zero.
  Proof.
(* Goal: forall _ : @In eill_cmd A Sig0, @ll_tps n s (eill_cmd_map A) (@vec_zero n) *)
    unfold Sig0.
(* Goal: forall _ : @In eill_cmd A (@cons eill_cmd (in_ll_cmd_inc (q k) (q k) (q k)) (@app eill_cmd (@map (prod (pos n) (pos n)) eill_cmd (fun c : prod (pos n) (pos n) => in_ll_cmd_dec (rx (@fst (pos n) (pos n) c)) (ry (@snd (pos n) (pos n) c)) (ry (@snd (pos n) (pos n) c))) (pos_not_diag n)) (@map (pos n) eill_cmd (fun j : pos n => in_ll_cmd_inc (ry j) (ry j) (ry j)) (pos_list n)))), @ll_tps n s (eill_cmd_map A) (@vec_zero n) *)
    intros [ H | H ]; subst. 
    
(* Goal: @ll_tps n s (eill_cmd_map (in_ll_cmd_inc (q k) (q k) (q k))) (@vec_zero n) *)
(* Goal: @ll_tps n s (eill_cmd_map A) (@vec_zero n) *)
    apply sem_k_k_k.
    
(* Goal: @ll_tps n s (eill_cmd_map A) (@vec_zero n) *)
    apply in_app_or in H.
    destruct H as [ H | H ]; 
    apply in_map_iff in H.
    
(* Goal: @ll_tps n s (eill_cmd_map A) (@vec_zero n) *)
(* Goal: @ll_tps n s (eill_cmd_map A) (@vec_zero n) *)
    destruct H as ((i & j) & H1 & H2); subst.
(* Goal: @ll_tps n s (eill_cmd_map (in_ll_cmd_dec (rx (@fst (pos n) (pos n) (@pair (pos n) (pos n) i j))) (ry (@snd (pos n) (pos n) (@pair (pos n) (pos n) i j))) (ry (@snd (pos n) (pos n) (@pair (pos n) (pos n) i j))))) (@vec_zero n) *)
(* Goal: @ll_tps n s (eill_cmd_map A) (@vec_zero n) *)
    apply sem_x_y_y; simpl.
(* Goal: not (@eq (pos n) i j) *)
(* Goal: @ll_tps n s (eill_cmd_map A) (@vec_zero n) *)
    apply pos_not_diag_spec in H2; auto.
    
(* Goal: @ll_tps n s (eill_cmd_map A) (@vec_zero n) *)
    destruct H as (y & H1 & _); subst.
(* Goal: @ll_tps n s (eill_cmd_map (in_ll_cmd_inc (ry y) (ry y) (ry y))) (@vec_zero n) *)
    apply sem_y_y_y.
  Qed.
  
  Let SigI_zero A : In A SigI -> [[ [iA] ]] vec_zero.
  Proof.
(* Goal: forall _ : @In eill_cmd A SigI, @ll_tps n s (eill_cmd_map A) (@vec_zero n) *)
    unfold SigI.
(* Goal: forall _ : @In eill_cmd A (let (i, l) := P in mm_linstr_enc i l), @ll_tps n s (eill_cmd_map A) (@vec_zero n) *)
    destruct P as (i & lP).
(* Goal: forall _ : @eq nat (@vec_pos nat n v p) O, G_eill Sig (@app nat (@vec_map_list nat n v rx) (@nil nat)) (ry p) *)
    intros H.
(* Goal: @ll_tps n s (eill_cmd_map A) (@vec_zero n) *)
    apply mm_linstr_enc_spec in H.
(* Goal: @ll_tps n s (eill_cmd_map A) (@vec_zero n) *)
    destruct H as [ (j & x & H1 & H2) | (j & x & p & H1 & [ H2 | H2 ]) ]; subst A.
    
(* Goal: @ll_tps n s (eill_cmd_map (in_ll_cmd_dec (rx x) (q (Init.Nat.add (S O) j)) (q j))) (@vec_zero n) *)
    simpl; unfold ll_tps_imp.
(* Goal: forall (x0 : vec nat n) (_ : forall (x1 : vec nat n) (_ : s (rx x) x1), s (q (S j)) (@vec_plus n x1 x0)), s (q j) (@vec_plus n x0 (@vec_zero n)) *)
(* Goal: @ll_tps n s (eill_cmd_map (in_ll_cmd_fork (ry x) (q p) (q j))) (@vec_zero n) *)
(* Goal: @ll_tps n s (eill_cmd_map (in_ll_cmd_dec (rx x) (q (Init.Nat.add (S O) j)) (q j))) (@vec_zero n) *)
    intros v Hv.
(* Goal: s (q j) (@vec_plus n v (@vec_zero n)) *)
(* Goal: @ll_tps n s (eill_cmd_map (in_ll_cmd_dec (rx x) (q (Init.Nat.add (S O) j)) (q j))) (@vec_zero n) *)
    rewrite vec_plus_comm, vec_zero_plus.
(* Goal: @sss_compute (mm_instr n) (vec nat n) (@mm_sss n) (@pair nat (list (mm_instr n)) i lP) (@pair nat (vec nat n) (Init.Nat.add (S O) j) (@vec_change nat n (@vec_plus n v w) x (@vec_pos nat n w x))) (@pair nat (vec nat n) k (@vec_zero n)) *)
    apply H_s_q.
(* Goal: @sss_compute (mm_instr n) (vec nat n) (@mm_sss n) (@pair nat (list (mm_instr n)) i lP) (@pair nat (vec nat n) j v) (@pair nat (vec nat n) k (@vec_zero n)) *)
(* Goal: @ll_tps n s (eill_cmd_map (in_ll_cmd_fork (ry x) (q p) (q j))) (@vec_zero n) *)
(* Goal: @ll_tps n s (eill_cmd_map (in_ll_cmd_dec (rx x) (q (Init.Nat.add (S O) j)) (q j))) (@vec_zero n) *)
    apply mm_compute_INC with (1 := H1).
(* Goal: @sss_compute (mm_instr n) (vec nat n) (@mm_sss n) (@pair nat (list (mm_instr n)) i lP) (@pair nat (vec nat n) (Init.Nat.add (S O) j) (@vec_change nat n v x (S (@vec_pos nat n v x)))) (@pair nat (vec nat n) k (@vec_zero n)) *)
(* Goal: @ll_tps n s (eill_cmd_map (in_ll_cmd_fork (ry x) (q p) (q j))) (@vec_zero n) *)
(* Goal: @ll_tps n s (eill_cmd_map (in_ll_cmd_dec (rx x) (q (Init.Nat.add (S O) j)) (q j))) (@vec_zero n) *)
    specialize (Hv (vec_one x)).
(* Goal: @sss_compute (mm_instr n) (vec nat n) (@mm_sss n) (@pair nat (list (mm_instr n)) i lP) (@pair nat (vec nat n) (Init.Nat.add (S O) j) (@vec_change nat n v x (S (@vec_pos nat n v x)))) (@pair nat (vec nat n) k (@vec_zero n)) *)
(* Goal: @ll_tps n s (eill_cmd_map (in_ll_cmd_fork (ry x) (q p) (q j))) (@vec_zero n) *)
(* Goal: @ll_tps n s (eill_cmd_map (in_ll_cmd_dec (rx x) (q (Init.Nat.add (S O) j)) (q j))) (@vec_zero n) *)
    replace (vec_change v x (S (vec_pos v x))) with (vec_plus (vec_one x) v).
(* Goal: @sss_compute (mm_instr n) (vec nat n) (@mm_sss n) (@pair nat (list (mm_instr n)) i lP) (@pair nat (vec nat n) (Init.Nat.add (S O) j) (@vec_change nat n (@vec_plus n v w) x (@vec_pos nat n w x))) (@pair nat (vec nat n) k (@vec_zero n)) *)
    apply H_s_q.
(* Goal: G_eill Sig0 (@app nat (@vec_map_list nat n v rx) (@app nat (@vec_map_list nat n w rx) Ga)) (ry p) *)
    apply Hv.
(* Goal: iff (@sss_compute (mm_instr n) (vec nat n) (@mm_sss n) P (@pair nat (vec nat n) i v) (@pair nat (vec nat n) k (@vec_zero n))) (G_eill Sig (@vec_map_list nat n v rx) (q i)) *)
    apply H_s_rx; split.
(* Goal: @eq (vec nat n) w (@vec_change nat n (@vec_plus n v w) x (@vec_pos nat n w x)) *)
    apply vec_pos_ext.
(* Goal: forall p : pos n, @eq nat (@vec_pos nat n (@vec_plus n (@vec_one n x) v) p) (@vec_pos nat n (@vec_change nat n v x (S (@vec_pos nat n v x))) p) *)
(* Goal: @ll_tps n s (eill_cmd_map (in_ll_cmd_fork (ry x) (q p) (q j))) (@vec_zero n) *)
(* Goal: @ll_tps n s (eill_cmd_map (in_ll_cmd_dec (rx x) (q (Init.Nat.add (S O) j)) (q j))) (@vec_zero n) *)
    intros p; rewrite vec_pos_plus.
(* Goal: @eq nat (Init.Nat.add (@vec_pos nat n (@vec_one n x) p) (@vec_pos nat n v p)) (@vec_pos nat n (@vec_change nat n v x (S (@vec_pos nat n v x))) p) *)
(* Goal: @ll_tps n s (eill_cmd_map (in_ll_cmd_fork (ry x) (q p) (q j))) (@vec_zero n) *)
(* Goal: @ll_tps n s (eill_cmd_map (in_ll_cmd_dec (rx x) (q (Init.Nat.add (S O) j)) (q j))) (@vec_zero n) *)
    destruct (pos_eq_dec x p).
(* Goal: @eq nat (Init.Nat.add (@vec_pos nat n (@vec_one n x) p) (@vec_pos nat n v p)) (@vec_pos nat n (@vec_change nat n v x (S (@vec_pos nat n v x))) p) *)
(* Goal: @eq nat (Init.Nat.add (@vec_pos nat n (@vec_one n x) p) (@vec_pos nat n v p)) (@vec_pos nat n (@vec_change nat n v x (S (@vec_pos nat n v x))) p) *)
(* Goal: @ll_tps n s (eill_cmd_map (in_ll_cmd_fork (ry x) (q p) (q j))) (@vec_zero n) *)
(* Goal: @ll_tps n s (eill_cmd_map (in_ll_cmd_dec (rx x) (q (Init.Nat.add (S O) j)) (q j))) (@vec_zero n) *)
    subst; rewrite vec_one_spec_eq, vec_change_eq; auto.
(* Goal: @eq nat (Init.Nat.add (@vec_pos nat n (@vec_one n x) p) (@vec_pos nat n v p)) (@vec_pos nat n (@vec_change nat n v x (S (@vec_pos nat n v x))) p) *)
(* Goal: @ll_tps n s (eill_cmd_map (in_ll_cmd_fork (ry x) (q p) (q j))) (@vec_zero n) *)
(* Goal: @ll_tps n s (eill_cmd_map (in_ll_cmd_dec (rx x) (q (Init.Nat.add (S O) j)) (q j))) (@vec_zero n) *)
    rewrite vec_one_spec_neq, vec_change_neq; auto.
    
(* Goal: @ll_tps n s (eill_cmd_map (in_ll_cmd_dec (rx x) (q (Init.Nat.add (S O) j)) (q j))) (@vec_zero n) *)
    simpl; unfold ll_tps_imp.
(* Goal: forall (x0 : vec nat n) (_ : and (s (ry x) x0) (s (q p) x0)), s (q j) (@vec_plus n x0 (@vec_zero n)) *)
(* Goal: @ll_tps n s (eill_cmd_map (in_ll_cmd_dec (rx x) (q (Init.Nat.add (S O) j)) (q j))) (@vec_zero n) *)
    intros v (Hv1 & Hv2).
(* Goal: s (q j) (@vec_plus n v (@vec_zero n)) *)
(* Goal: @ll_tps n s (eill_cmd_map (in_ll_cmd_dec (rx x) (q (Init.Nat.add (S O) j)) (q j))) (@vec_zero n) *)
    rewrite vec_plus_comm, vec_zero_plus.
(* Goal: @sss_compute (mm_instr n) (vec nat n) (@mm_sss n) (@pair nat (list (mm_instr n)) i lP) (@pair nat (vec nat n) (Init.Nat.add (S O) j) (@vec_change nat n (@vec_plus n v w) x (@vec_pos nat n w x))) (@pair nat (vec nat n) k (@vec_zero n)) *)
    apply H_s_q.
(* Goal: @sss_compute (mm_instr n) (vec nat n) (@mm_sss n) (@pair nat (list (mm_instr n)) i lP) (@pair nat (vec nat n) j v) (@pair nat (vec nat n) k (@vec_zero n)) *)
(* Goal: @ll_tps n s (eill_cmd_map (in_ll_cmd_dec (rx x) (q (Init.Nat.add (S O) j)) (q j))) (@vec_zero n) *)
    rewrite H_s_ry in Hv1.
(* Goal: @sss_compute (mm_instr n) (vec nat n) (@mm_sss n) (@pair nat (list (mm_instr n)) i lP) (@pair nat (vec nat n) j v) (@pair nat (vec nat n) k (@vec_zero n)) *)
(* Goal: @ll_tps n s (eill_cmd_map (in_ll_cmd_dec (rx x) (q (Init.Nat.add (S O) j)) (q j))) (@vec_zero n) *)
    apply mm_compute_DEC_0 with (1 := H1); auto.
(* Goal: @sss_compute (mm_instr n) (vec nat n) (@mm_sss n) P (@pair nat (vec nat n) i v) (@pair nat (vec nat n) k (@vec_zero n)) *)
    apply H_s_q; auto.
    
(* Goal: @ll_tps n s (eill_cmd_map (in_ll_cmd_dec (rx x) (q (Init.Nat.add (S O) j)) (q j))) (@vec_zero n) *)
    simpl; unfold ll_tps_imp.
(* Goal: forall (x0 : vec nat n) (_ : s (rx x) x0) (x : vec nat n) (_ : s (q (S j)) x), s (q j) (@vec_plus n x (@vec_plus n x0 (@vec_zero n))) *)
    intros v Hv w Hw.
(* Goal: s (q j) (@vec_plus n w (@vec_plus n v (@vec_zero n))) *)
    rewrite (vec_plus_comm v), vec_zero_plus.
(* Goal: @sss_compute (mm_instr n) (vec nat n) (@mm_sss n) (@pair nat (list (mm_instr n)) i lP) (@pair nat (vec nat n) (Init.Nat.add (S O) j) (@vec_change nat n (@vec_plus n v w) x (@vec_pos nat n w x))) (@pair nat (vec nat n) k (@vec_zero n)) *)
    apply H_s_q.
(* Goal: @sss_compute (mm_instr n) (vec nat n) (@mm_sss n) (@pair nat (list (mm_instr n)) i lP) (@pair nat (vec nat n) j (@vec_plus n w v)) (@pair nat (vec nat n) k (@vec_zero n)) *)
    apply H_s_rx in Hv.
(* Goal: @sss_compute (mm_instr n) (vec nat n) (@mm_sss n) (@pair nat (list (mm_instr n)) i lP) (@pair nat (vec nat n) j (@vec_plus n w v)) (@pair nat (vec nat n) k (@vec_zero n)) *)
    rewrite vec_plus_comm.
(* Goal: @sss_compute (mm_instr n) (vec nat n) (@mm_sss n) (@pair nat (list (mm_instr n)) i lP) (@pair nat (vec nat n) j (@vec_plus n v w)) (@pair nat (vec nat n) k (@vec_zero n)) *)
    assert (exists u, vec_pos (vec_plus v w) x = S u) as Hu.
(* Goal: @ex nat (fun u : nat => @eq nat (@vec_pos nat n (@vec_plus n v w) x) (S u)) *)
(* Goal: @sss_compute (mm_instr n) (vec nat n) (@mm_sss n) (@pair nat (list (mm_instr n)) i lP) (@pair nat (vec nat n) j (@vec_plus n v w)) (@pair nat (vec nat n) k (@vec_zero n)) *)
      exists (vec_pos w x).
(* Goal: @eq nat (@vec_pos nat n (@vec_plus n v w) x) (S (@vec_pos nat n w x)) *)
(* Goal: @sss_compute (mm_instr n) (vec nat n) (@mm_sss n) (@pair nat (list (mm_instr n)) i lP) (@pair nat (vec nat n) (Init.Nat.add (S O) j) (@vec_change nat n (@vec_plus n v w) x (@vec_pos nat n w x))) (@pair nat (vec nat n) k (@vec_zero n)) *)
      rewrite vec_pos_plus; subst.
(* Goal: @eq nat (Init.Nat.add (@vec_pos nat n (@vec_one n x) x) (@vec_pos nat n w x)) (S (@vec_pos nat n w x)) *)
(* Goal: @sss_compute (mm_instr n) (vec nat n) (@mm_sss n) (@pair nat (list (mm_instr n)) i lP) (@pair nat (vec nat n) (Init.Nat.add (S O) j) (@vec_change nat n (@vec_plus n v w) x (@vec_pos nat n w x))) (@pair nat (vec nat n) k (@vec_zero n)) *)
      rewrite vec_one_spec_eq; auto.
(* Goal: @sss_compute (mm_instr n) (vec nat n) (@mm_sss n) (@pair nat (list (mm_instr n)) i lP) (@pair nat (vec nat n) j (@vec_plus n v w)) (@pair nat (vec nat n) k (@vec_zero n)) *)
    destruct Hu as (u & Hu).
(* Goal: @sss_compute (mm_instr n) (vec nat n) (@mm_sss n) (@pair nat (list (mm_instr n)) i lP) (@pair nat (vec nat n) j (@vec_plus n v w)) (@pair nat (vec nat n) k (@vec_zero n)) *)
    apply mm_compute_DEC_S with (1 := H1) (u := vec_pos w x); auto.
(* Goal: @eq nat (@vec_pos nat n (@vec_plus n v w) x) (S (@vec_pos nat n w x)) *)
(* Goal: @sss_compute (mm_instr n) (vec nat n) (@mm_sss n) (@pair nat (list (mm_instr n)) i lP) (@pair nat (vec nat n) (Init.Nat.add (S O) j) (@vec_change nat n (@vec_plus n v w) x (@vec_pos nat n w x))) (@pair nat (vec nat n) k (@vec_zero n)) *)
    rewrite vec_pos_plus; subst.
(* Goal: @eq nat (Init.Nat.add (@vec_pos nat n (@vec_one n x) x) (@vec_pos nat n w x)) (S (@vec_pos nat n w x)) *)
(* Goal: @sss_compute (mm_instr n) (vec nat n) (@mm_sss n) (@pair nat (list (mm_instr n)) i lP) (@pair nat (vec nat n) (Init.Nat.add (S O) j) (@vec_change nat n (@vec_plus n v w) x (@vec_pos nat n w x))) (@pair nat (vec nat n) k (@vec_zero n)) *)
    rewrite vec_one_spec_eq; auto.
(* Goal: @sss_compute (mm_instr n) (vec nat n) (@mm_sss n) (@pair nat (list (mm_instr n)) i lP) (@pair nat (vec nat n) (Init.Nat.add (S O) j) (@vec_change nat n (@vec_plus n v w) x (@vec_pos nat n w x))) (@pair nat (vec nat n) k (@vec_zero n)) *)
    apply H_s_q.
(* Goal: s (q (Init.Nat.add (S O) j)) (@vec_change nat n (@vec_plus n v w) x (@vec_pos nat n w x)) *)
    eq goal Hw; f_equal.
(* Goal: @eq (vec nat n) w (@vec_change nat n (@vec_plus n v w) x (@vec_pos nat n w x)) *)
    apply vec_pos_ext.
(* Goal: forall p : pos n, @eq nat (@vec_pos nat n w p) (@vec_pos nat n (@vec_change nat n (@vec_plus n v w) x (@vec_pos nat n w x)) p) *)
    intros r.
(* Goal: @eq nat (@vec_pos nat n w r) (@vec_pos nat n (@vec_change nat n (@vec_plus n v w) x (@vec_pos nat n w x)) r) *)
    destruct (pos_eq_dec x r).
(* Goal: @eq nat (@vec_pos nat n w r) (@vec_pos nat n (@vec_change nat n (@vec_plus n v w) x (@vec_pos nat n w x)) r) *)
(* Goal: @eq nat (@vec_pos nat n w r) (@vec_pos nat n (@vec_change nat n (@vec_plus n v w) x (@vec_pos nat n w x)) r) *)
    subst; rewrite vec_change_eq; auto.
(* Goal: @eq nat (@vec_pos nat n w r) (@vec_pos nat n (@vec_change nat n (@vec_plus n v w) x (@vec_pos nat n w x)) r) *)
    rewrite vec_change_neq, vec_pos_plus; auto.
(* Goal: @eq nat (@vec_pos nat n w r) (Init.Nat.add (@vec_pos nat n v r) (@vec_pos nat n w r)) *)
    subst; rewrite vec_one_spec_neq; auto.
  Qed.
 
  Lemma Sig_zero A : In A Sig -> [[ [i A] ]] vec_zero.
  Proof.
(* Goal: forall _ : @In eill_cmd A Sig, @ll_tps n s (eill_cmd_map A) (@vec_zero n) *)
    intros H; apply in_app_or in H; destruct H.
(* Goal: @ll_tps n s (eill_cmd_map A) (@vec_zero n) *)
(* Goal: @ll_tps n s (eill_cmd_map A) (@vec_zero n) *)
    apply Sig0_zero; auto.
(* Goal: @ll_tps n s (eill_cmd_map A) (@vec_zero n) *)
    apply SigI_zero; auto.
  Qed.
  
  Corollary ll_tps_Sig_zero : ll_tps_list s (map (fun c => ❗[i c]) Sig) vec_zero.
  Proof.
(* Goal: @ll_tps_list n s (@map eill_cmd ll_form (fun c : eill_cmd => ll_ban (eill_cmd_map c)) Sig) (@vec_zero n) *)
    generalize Sig Sig_zero; intros S.
(* Goal: forall _ : forall (A : eill_cmd) (_ : @In eill_cmd A S), @ll_tps n s (eill_cmd_map A) (@vec_zero n), @ll_tps_list n s (@map eill_cmd ll_form (fun c : eill_cmd => ll_ban (eill_cmd_map c)) S) (@vec_zero n) *)
    induction S as [ | A S IHS ]; intros HS.
(* Goal: @ll_tps_list n s (@map eill_cmd ll_form (fun c : eill_cmd => ll_ban (eill_cmd_map c)) (@nil eill_cmd)) (@vec_zero n) *)
(* Goal: @ll_tps_list n s (@map eill_cmd ll_form (fun c : eill_cmd => ll_ban (eill_cmd_map c)) (@cons eill_cmd A S)) (@vec_zero n) *)
    simpl; auto.
(* Goal: @ll_tps_list n s (@map eill_cmd ll_form (fun c : eill_cmd => ll_ban (eill_cmd_map c)) (@cons eill_cmd A S)) (@vec_zero n) *)
    simpl; exists vec_zero, vec_zero; repeat split; auto.
(* Goal: @eq (vec nat n) v (@vec_plus n (@vec_zero n) v) *)
(* Goal: @ll_tps_list n s (@map eill_cmd ll_form (fun c : eill_cmd => ll_ban (eill_cmd_map c)) Sig) (@vec_zero n) *)
(* Goal: @ll_tps_list n s (@map ill.ll_vars ll_form ll_var (@vec_map_list nat n v rx)) v *)
    rew vec.
(* Goal: @ll_tps n s (eill_cmd_map A) (@vec_zero n) *)
(* Goal: @ll_tps_list n s (@map eill_cmd ll_form (fun c : eill_cmd => ll_ban (eill_cmd_map c)) S) (@vec_zero n) *)
    apply HS; left; auto.
(* Goal: @ll_tps_list n s (@map eill_cmd ll_form (fun c : eill_cmd => ll_ban (eill_cmd_map c)) S) (@vec_zero n) *)
    apply IHS; intros; apply HS; right; auto.
  Qed.
 
  Theorem lemma_5_5 v i : Sig; vec_map_list v rx ⊦ q i -> P // (i,v) ->> (k,vec_zero).
  Proof.
(* Goal: forall _ : @eq nat (@vec_pos nat n v p) O, G_eill Sig (@app nat (@vec_map_list nat n v rx) (@nil nat)) (ry p) *)
    intros H.
(* Goal: @sss_compute (mm_instr n) (vec nat n) (@mm_sss n) P (@pair nat (vec nat n) i v) (@pair nat (vec nat n) k (@vec_zero n)) *)
    apply G_eill_sound in H.
(* Goal: @sss_compute (mm_instr n) (vec nat n) (@mm_sss n) P (@pair nat (vec nat n) i v) (@pair nat (vec nat n) k (@vec_zero n)) *)
    apply ll_tps_sound with (s := s) in H.
(* Goal: @sss_compute (mm_instr n) (vec nat n) (@mm_sss n) P (@pair nat (vec nat n) i v) (@pair nat (vec nat n) k (@vec_zero n)) *)
    red in H.
(* Goal: @sss_compute (mm_instr n) (vec nat n) (@mm_sss n) P (@pair nat (vec nat n) i v) (@pair nat (vec nat n) k (@vec_zero n)) *)
    specialize (H v).
(* Goal: @sss_compute (mm_instr n) (vec nat n) (@mm_sss n) P (@pair nat (vec nat n) i v) (@pair nat (vec nat n) k (@vec_zero n)) *)
    rewrite vec_plus_comm, vec_zero_plus in H.
(* Goal: @sss_compute (mm_instr n) (vec nat n) (@mm_sss n) P (@pair nat (vec nat n) i v) (@pair nat (vec nat n) k (@vec_zero n)) *)
    apply H_s_q; auto.
(* Goal: s (q i) v *)
    apply H.
(* Goal: @ll_tps_list n s (@app ll_form (@map eill_cmd ll_form (fun c : eill_cmd => ll_ban (eill_cmd_map c)) Sig) (@map ill.ll_vars ll_form ll_var (@vec_map_list nat n v rx))) v *)
    rewrite ll_tps_app.
(* Goal: iff (@sss_compute (mm_instr n) (vec nat n) (@mm_sss n) P (@pair nat (vec nat n) i v) (@pair nat (vec nat n) k (@vec_zero n))) (G_eill Sig (@vec_map_list nat n v rx) (q i)) *)
    exists vec_zero, v; repeat split.
(* Goal: @eq (vec nat n) v (@vec_plus n (@vec_zero n) v) *)
(* Goal: @ll_tps_list n s (@map eill_cmd ll_form (fun c : eill_cmd => ll_ban (eill_cmd_map c)) Sig) (@vec_zero n) *)
(* Goal: @ll_tps_list n s (@map ill.ll_vars ll_form ll_var (@vec_map_list nat n v rx)) v *)
    rew vec.
(* Goal: @ll_tps_list n s (@map eill_cmd ll_form (fun c : eill_cmd => ll_ban (eill_cmd_map c)) Sig) (@vec_zero n) *)
(* Goal: @ll_tps_list n s (@map ill.ll_vars ll_form ll_var (@vec_map_list nat n v rx)) v *)
    apply ll_tps_Sig_zero.
(* Goal: @ll_tps_list n s (@map ill.ll_vars ll_form ll_var (@vec_map_list nat n v rx)) v *)
    apply ll_tps_vec_map_list; auto.
  Qed.
  
  Let prop_5_2_rec (p : pos n) v Ga : 
         vec_pos v p = 0 
      -> Sig0;                      Ga ⊦ ry p 
      -> Sig0; vec_map_list v rx ++ Ga ⊦ ry p.
  Proof.
(* Goal: forall (_ : @eq nat (@vec_pos nat n v p) O) (_ : G_eill Sig0 Ga (ry p)), G_eill Sig0 (@app nat (@vec_map_list nat n v rx) Ga) (ry p) *)
    revert Ga.
(* Goal: forall (Ga : list ll_vars) (_ : @eq nat (@vec_pos nat n v p) O) (_ : G_eill Sig0 Ga (ry p)), G_eill Sig0 (@app nat (@vec_map_list nat n v rx) Ga) (ry p) *)
    induction v as [ | r | v w Hv Hw ] using (@vec_nat_induction _); intros Ga.

(* Goal: forall (_ : @eq nat (@vec_pos nat n (@vec_zero n) p) O) (_ : G_eill Sig0 Ga (ry p)), G_eill Sig0 (@app nat (@vec_map_list nat n (@vec_zero n) rx) Ga) (ry p) *)
(* Goal: forall (_ : @eq nat (@vec_pos nat n (@vec_one n r) p) O) (_ : G_eill Sig0 Ga (ry p)), G_eill Sig0 (@app nat (@vec_map_list nat n (@vec_one n r) rx) Ga) (ry p) *)
(* Goal: forall (_ : @eq nat (@vec_pos nat n (@vec_plus n v w) p) O) (_ : G_eill Sig0 Ga (ry p)), G_eill Sig0 (@app nat (@vec_map_list nat n (@vec_plus n v w) rx) Ga) (ry p) *)
    intros _.
(* Goal: G_eill Sig (@vec_map_list nat n (@vec_zero n) rx) (q k) *)
(* Goal: G_eill Sig (@vec_map_list nat n v rx) (q i) *)
    rewrite vec_map_list_zero.
(* Goal: forall _ : G_eill Sig0 Ga (ry p), G_eill Sig0 (@app nat (@nil nat) Ga) (ry p) *)
(* Goal: forall (_ : @eq nat (@vec_pos nat n (@vec_one n r) p) O) (_ : G_eill Sig0 Ga (ry p)), G_eill Sig0 (@app nat (@vec_map_list nat n (@vec_one n r) rx) Ga) (ry p) *)
(* Goal: forall (_ : @eq nat (@vec_pos nat n (@vec_plus n v w) p) O) (_ : G_eill Sig0 Ga (ry p)), G_eill Sig0 (@app nat (@vec_map_list nat n (@vec_plus n v w) rx) Ga) (ry p) *)
    auto.
    
(* Goal: @eq (vec nat n) v (@vec_plus n (@vec_zero n) v) *)
(* Goal: @ll_tps_list n s (@map eill_cmd ll_form (fun c : eill_cmd => ll_ban (eill_cmd_map c)) Sig) (@vec_zero n) *)
(* Goal: @ll_tps_list n s (@map ill.ll_vars ll_form ll_var (@vec_map_list nat n v rx)) v *)
    destruct (pos_eq_dec r p) as [ H | H ]; rew vec.
(* Goal: @eq nat (@vec_pos nat n v p) O *)
(* Goal: G_eill Sig0 (@app nat (@vec_map_list nat n w rx) Ga) (ry p) *)
    omega.
(* Goal: forall (_ : @eq nat O O) (_ : G_eill Sig0 Ga (ry p)), G_eill Sig0 (@app nat (@vec_map_list nat n (@vec_one n r) rx) Ga) (ry p) *)
(* Goal: forall (_ : @eq nat (@vec_pos nat n (@vec_plus n v w) p) O) (_ : G_eill Sig0 Ga (ry p)), G_eill Sig0 (@app nat (@vec_map_list nat n (@vec_plus n v w) rx) Ga) (ry p) *)
    intros _ H1.
(* Goal: G_eill Sig (@app ll_vars (@vec_map_list ll_vars n (@vec_one n p) rx) (@vec_map_list ll_vars n (@vec_change nat n v p u) rx)) (q i) *)
    rewrite vec_map_list_one.
(* Goal: forall _ : G_eill Sig0 Ga (ry p), G_eill Sig0 (@app nat (@nil nat) Ga) (ry p) *)
(* Goal: forall (_ : @eq nat (@vec_pos nat n (@vec_one n r) p) O) (_ : G_eill Sig0 Ga (ry p)), G_eill Sig0 (@app nat (@vec_map_list nat n (@vec_one n r) rx) Ga) (ry p) *)
(* Goal: forall (_ : @eq nat (@vec_pos nat n (@vec_plus n v w) p) O) (_ : G_eill Sig0 Ga (ry p)), G_eill Sig0 (@app nat (@vec_map_list nat n (@vec_plus n v w) rx) Ga) (ry p) *)
    apply in_eill_dec with (rx r) (ry p); auto.
(* Goal: @In eill_cmd (in_ll_cmd_dec (rx r) (ry p) (ry p)) Sig0 *)
(* Goal: G_eill Sig0 (@cons nat (rx r) (@nil nat)) (rx r) *)
(* Goal: forall (_ : @eq nat (@vec_pos nat n (@vec_plus n v w) p) O) (_ : G_eill Sig0 Ga (ry p)), G_eill Sig0 (@app nat (@vec_map_list nat n (@vec_plus n v w) rx) Ga) (ry p) *)
    right; apply in_or_app; left.
(* Goal: @In eill_cmd (in_ll_cmd_inc (ry p) (ry p) (ry p)) (@map (pos n) eill_cmd (fun j : pos n => in_ll_cmd_inc (ry j) (ry j) (ry j)) (pos_list n)) *)
(* Goal: G_eill Sig0 (@cons ll_vars (ry p) (@nil nat)) (ry p) *)
    apply in_map_iff.
(* Goal: forall _ : G_eill Sig0 Ga (ry p), G_eill Sig0 (@app nat (@nil nat) Ga) (ry p) *)
(* Goal: forall (_ : @eq nat (@vec_pos nat n (@vec_one n r) p) O) (_ : G_eill Sig0 Ga (ry p)), G_eill Sig0 (@app nat (@vec_map_list nat n (@vec_one n r) rx) Ga) (ry p) *)
(* Goal: forall (_ : @eq nat (@vec_pos nat n (@vec_plus n v w) p) O) (_ : G_eill Sig0 Ga (ry p)), G_eill Sig0 (@app nat (@vec_map_list nat n (@vec_plus n v w) rx) Ga) (ry p) *)
    exists (r,p); simpl; split; auto.
(* Goal: forall _ : G_eill Sig0 Ga (ry p), G_eill Sig0 (@app nat (@nil nat) Ga) (ry p) *)
(* Goal: forall (_ : @eq nat (@vec_pos nat n (@vec_one n r) p) O) (_ : G_eill Sig0 Ga (ry p)), G_eill Sig0 (@app nat (@vec_map_list nat n (@vec_one n r) rx) Ga) (ry p) *)
(* Goal: forall (_ : @eq nat (@vec_pos nat n (@vec_plus n v w) p) O) (_ : G_eill Sig0 Ga (ry p)), G_eill Sig0 (@app nat (@vec_map_list nat n (@vec_plus n v w) rx) Ga) (ry p) *)
    apply pos_not_diag_spec; auto.
(* Goal: G_eill Sig (@cons ll_vars (rx p) (@nil ll_vars)) (rx p) *)
    apply in_eill_ax.
    
(* Goal: forall (_ : @eq nat (@vec_pos nat n (@vec_plus n v w) p) O) (_ : G_eill Sig0 Ga (ry p)), G_eill Sig0 (@app nat (@vec_map_list nat n (@vec_plus n v w) rx) Ga) (ry p) *)
    intros H1 H2.
(* Goal: G_eill Sig0 (@app nat (@vec_map_list nat n (@vec_plus n v w) rx) Ga) (ry p) *)
    rewrite vec_pos_plus in H1.
(* Goal: G_eill Sig0 (@app nat (@vec_map_list nat n (@vec_plus n v w) rx) Ga) (ry p) *)
    apply in_eill_perm with (vec_map_list v rx ++ vec_map_list w rx ++ Ga).
(* Goal: forall _ : G_eill Sig0 Ga (ry p), G_eill Sig0 (@app nat (@nil nat) Ga) (ry p) *)
(* Goal: forall (_ : @eq nat (@vec_pos nat n (@vec_one n r) p) O) (_ : G_eill Sig0 Ga (ry p)), G_eill Sig0 (@app nat (@vec_map_list nat n (@vec_one n r) rx) Ga) (ry p) *)
(* Goal: forall (_ : @eq nat (@vec_pos nat n (@vec_plus n v w) p) O) (_ : G_eill Sig0 Ga (ry p)), G_eill Sig0 (@app nat (@vec_map_list nat n (@vec_plus n v w) rx) Ga) (ry p) *)
    rewrite vec_map_list_plus, app_ass; auto.
(* Goal: G_eill Sig0 (@app nat (@vec_map_list nat n v rx) (@app nat (@vec_map_list nat n w rx) Ga)) (ry p) *)
    apply Hv.
(* Goal: @eq nat (@vec_pos nat n v p) O *)
(* Goal: G_eill Sig0 (@app nat (@vec_map_list nat n w rx) Ga) (ry p) *)
    omega.
(* Goal: @eq nat (@vec_pos nat n v p) O *)
(* Goal: G_eill Sig0 (@app nat (@vec_map_list nat n w rx) Ga) (ry p) *)
    apply Hw; auto; omega.
  Qed.
  
  Lemma prop_5_2 p v : 
           vec_pos v p = 0 
        -> Sig; vec_map_list v rx ⊦ ry p.
  Proof.
(* Goal: forall _ : @eq nat (@vec_pos nat n v p) O, G_eill Sig (@vec_map_list nat n v rx) (ry p) *)
    rewrite (app_nil_end (_ _ rx)).
(* Goal: forall _ : @eq nat (@vec_pos nat n v p) O, G_eill Sig (@app nat (@vec_map_list nat n v rx) (@nil nat)) (ry p) *)
    intros H.
(* Goal: G_eill Sig (@app nat (@vec_map_list nat n v rx) (@nil nat)) (ry p) *)
    apply g_eill_mono_Si with Sig0.
(* Goal: forall _ : G_eill Sig0 Ga (ry p), G_eill Sig0 (@app nat (@nil nat) Ga) (ry p) *)
(* Goal: forall (_ : @eq nat (@vec_pos nat n (@vec_one n r) p) O) (_ : G_eill Sig0 Ga (ry p)), G_eill Sig0 (@app nat (@vec_map_list nat n (@vec_one n r) rx) Ga) (ry p) *)
(* Goal: forall (_ : @eq nat (@vec_pos nat n (@vec_plus n v w) p) O) (_ : G_eill Sig0 Ga (ry p)), G_eill Sig0 (@app nat (@vec_map_list nat n (@vec_plus n v w) rx) Ga) (ry p) *)
    unfold Sig; intros ? ?; apply in_or_app; left; auto.
(* Goal: forall _ : G_eill Sig0 Ga (ry p), G_eill Sig0 (@app nat (@nil nat) Ga) (ry p) *)
(* Goal: forall (_ : @eq nat (@vec_pos nat n (@vec_one n r) p) O) (_ : G_eill Sig0 Ga (ry p)), G_eill Sig0 (@app nat (@vec_map_list nat n (@vec_one n r) rx) Ga) (ry p) *)
(* Goal: forall (_ : @eq nat (@vec_pos nat n (@vec_plus n v w) p) O) (_ : G_eill Sig0 Ga (ry p)), G_eill Sig0 (@app nat (@vec_map_list nat n (@vec_plus n v w) rx) Ga) (ry p) *)
    apply prop_5_2_rec; auto.
(* Goal: G_eill Sig0 (@nil nat) (ry p) *)
    apply in_eill_inc with (ry p) (ry p).
(* Goal: @In eill_cmd (in_ll_cmd_inc (ry p) (ry p) (ry p)) Sig0 *)
(* Goal: G_eill Sig0 (@cons ll_vars (ry p) (@nil nat)) (ry p) *)
    right; apply in_or_app; right.
(* Goal: @In eill_cmd (in_ll_cmd_inc (ry p) (ry p) (ry p)) (@map (pos n) eill_cmd (fun j : pos n => in_ll_cmd_inc (ry j) (ry j) (ry j)) (pos_list n)) *)
(* Goal: G_eill Sig0 (@cons ll_vars (ry p) (@nil nat)) (ry p) *)
    apply in_map_iff.
(* Goal: forall _ : G_eill Sig0 Ga (ry p), G_eill Sig0 (@app nat (@nil nat) Ga) (ry p) *)
(* Goal: forall (_ : @eq nat (@vec_pos nat n (@vec_one n r) p) O) (_ : G_eill Sig0 Ga (ry p)), G_eill Sig0 (@app nat (@vec_map_list nat n (@vec_one n r) rx) Ga) (ry p) *)
(* Goal: forall (_ : @eq nat (@vec_pos nat n (@vec_plus n v w) p) O) (_ : G_eill Sig0 Ga (ry p)), G_eill Sig0 (@app nat (@vec_map_list nat n (@vec_plus n v w) rx) Ga) (ry p) *)
    exists p; split; auto.
(* Goal: @In (pos n) p (pos_list n) *)
(* Goal: G_eill Sig0 (@cons ll_vars (ry p) (@nil nat)) (ry p) *)
    apply pos_list_prop.
(* Goal: G_eill Sig (@cons ll_vars (rx p) (@nil ll_vars)) (rx p) *)
    apply in_eill_ax.
  Qed.
  
  Lemma lemma_5_3 i v : P // (i,v) ->> (k,vec_zero) -> Sig; vec_map_list v rx ⊦ q i.
  Proof.
(* Goal: forall _ : @sss_compute (mm_instr n) (vec nat n) (@mm_sss n) P (@pair nat (vec nat n) i v) (@pair nat (vec nat n) k (@vec_zero n)), G_eill Sig (@vec_map_list nat n v rx) (q i) *)
    intros (r & Hr); revert i v Hr.
(* Goal: forall (i : nat) (v : vec nat n) (_ : @sss_steps (mm_instr n) (vec nat n) (@mm_sss n) P r (@pair nat (vec nat n) i v) (@pair nat (vec nat n) k (@vec_zero n))), G_eill Sig (@vec_map_list nat n v rx) (q i) *)
    induction r as [ | r IHr ]; intros i v Hr.
    
(* Goal: G_eill Sig (@vec_map_list nat n v rx) (q i) *)
(* Goal: G_eill Sig (@vec_map_list nat n v rx) (q i) *)
    apply sss_steps_0_inv in Hr.
(* Goal: G_eill Sig (@vec_map_list nat n v rx) (q i) *)
(* Goal: G_eill Sig (@vec_map_list nat n v rx) (q i) *)
    inversion Hr; subst i v; clear Hr.
(* Goal: G_eill Sig (@vec_map_list nat n (@vec_zero n) rx) (q k) *)
(* Goal: G_eill Sig (@vec_map_list nat n v rx) (q i) *)
    rewrite vec_map_list_zero.
(* Goal: G_eill Sig (@nil nat) (q k) *)
(* Goal: G_eill Sig (@vec_map_list nat n v rx) (q i) *)
    apply in_eill_inc with (q k) (q k).
(* Goal: forall _ : G_eill Sig0 Ga (ry p), G_eill Sig0 (@app nat (@nil nat) Ga) (ry p) *)
(* Goal: forall (_ : @eq nat (@vec_pos nat n (@vec_one n r) p) O) (_ : G_eill Sig0 Ga (ry p)), G_eill Sig0 (@app nat (@vec_map_list nat n (@vec_one n r) rx) Ga) (ry p) *)
(* Goal: forall (_ : @eq nat (@vec_pos nat n (@vec_plus n v w) p) O) (_ : G_eill Sig0 Ga (ry p)), G_eill Sig0 (@app nat (@vec_map_list nat n (@vec_plus n v w) rx) Ga) (ry p) *)
    left; auto.
(* Goal: G_eill Sig (@cons ll_vars (rx p) (@nil ll_vars)) (rx p) *)
    apply in_eill_ax.
    
(* Goal: G_eill Sig (@vec_map_list nat n v rx) (q i) *)
    apply sss_steps_S_inv' in Hr.
(* Goal: G_eill Sig (@vec_map_list nat n v rx) (q i) *)
    destruct Hr as ((j,w) & H1 & H2).
(* Goal: G_eill Sig (@vec_map_list nat n v rx) (q i) *)
    apply IHr in H2.
(* Goal: G_eill Sig (@vec_map_list nat n v rx) (q i) *)
    generalize (sss_step_in_code H1); simpl fst; intros H3.
(* Goal: G_eill Sig (@vec_map_list nat n v rx) (q i) *)
    apply in_code_subcode in H3.
(* Goal: G_eill Sig (@vec_map_list nat n v rx) (q i) *)
    destruct H3 as (ii & Hii).
(* Goal: G_eill Sig (@vec_map_list nat n v rx) (q i) *)
    apply sss_step_subcode_inv with (1 := Hii) in H1.
(* Goal: G_eill Sig (@vec_map_list nat n v rx) (q i) *)
    destruct ii as [ p | p l ].
    
(* Goal: G_eill Sig (@vec_map_list nat n v rx) (q i) *)
(* Goal: G_eill Sig (@vec_map_list nat n v rx) (q i) *)
    apply mm_sss_INC_inv in H1.
(* Goal: G_eill Sig (@vec_map_list nat n v rx) (q i) *)
(* Goal: G_eill Sig (@vec_map_list nat n v rx) (q i) *)
    destruct H1; subst.
(* Goal: G_eill Sig (@vec_map_list nat n v rx) (q i) *)
(* Goal: G_eill Sig (@vec_map_list nat n v rx) (q i) *)
    apply in_eill_inc with (rx p) (q (1+i)).
(* Goal: @In eill_cmd (in_ll_cmd_dec (rx p) (q (Init.Nat.add (S O) i)) (q i)) Sig *)
(* Goal: G_eill Sig (@cons ll_vars (rx p) (@nil ll_vars)) (rx p) *)
    apply in_or_app; right.
(* Goal: @In eill_cmd (in_ll_cmd_dec (rx p) (q (Init.Nat.add (S O) i)) (q i)) SigI *)
(* Goal: G_eill Sig (@cons ll_vars (rx p) (@nil ll_vars)) (rx p) *)
    unfold SigI; destruct P as (ip,lP).
(* Goal: forall _ : G_eill Sig0 Ga (ry p), G_eill Sig0 (@app nat (@nil nat) Ga) (ry p) *)
(* Goal: forall (_ : @eq nat (@vec_pos nat n (@vec_one n r) p) O) (_ : G_eill Sig0 Ga (ry p)), G_eill Sig0 (@app nat (@vec_map_list nat n (@vec_one n r) rx) Ga) (ry p) *)
(* Goal: forall (_ : @eq nat (@vec_pos nat n (@vec_plus n v w) p) O) (_ : G_eill Sig0 Ga (ry p)), G_eill Sig0 (@app nat (@vec_map_list nat n (@vec_plus n v w) rx) Ga) (ry p) *)
    apply subcode_mm_linstr_enc; auto.
(* Goal: G_eill Sig (@cons ll_vars (rx p) (@vec_map_list nat n v rx)) (q (Init.Nat.add (S O) i)) *)
(* Goal: G_eill Sig (@vec_map_list nat n v rx) (q i) *)
    revert H2; apply in_eill_perm.
(* Goal: forall _ : G_eill Sig0 Ga (ry p), G_eill Sig0 (@app nat (@nil nat) Ga) (ry p) *)
(* Goal: forall (_ : @eq nat (@vec_pos nat n (@vec_one n r) p) O) (_ : G_eill Sig0 Ga (ry p)), G_eill Sig0 (@app nat (@vec_map_list nat n (@vec_one n r) rx) Ga) (ry p) *)
(* Goal: forall (_ : @eq nat (@vec_pos nat n (@vec_plus n v w) p) O) (_ : G_eill Sig0 Ga (ry p)), G_eill Sig0 (@app nat (@vec_map_list nat n (@vec_plus n v w) rx) Ga) (ry p) *)
    rewrite vec_change_succ, vec_map_list_plus, vec_map_list_one; auto.
    
(* Goal: G_eill Sig (@vec_map_list nat n v rx) (q i) *)
    case_eq (vec_pos v p).
    
(* Goal: forall _ : @eq nat (@vec_pos nat n v p) O, G_eill Sig (@vec_map_list nat n v rx) (q i) *)
(* Goal: forall (n0 : nat) (_ : @eq nat (@vec_pos nat n v p) (S n0)), G_eill Sig (@vec_map_list nat n v rx) (q i) *)
    intros Hv.
(* Goal: forall _ : G_eill Sig0 Ga (ry p), G_eill Sig0 (@app nat (@nil nat) Ga) (ry p) *)
(* Goal: forall (_ : @eq nat (@vec_pos nat n (@vec_one n r) p) O) (_ : G_eill Sig0 Ga (ry p)), G_eill Sig0 (@app nat (@vec_map_list nat n (@vec_one n r) rx) Ga) (ry p) *)
(* Goal: forall (_ : @eq nat (@vec_pos nat n (@vec_plus n v w) p) O) (_ : G_eill Sig0 Ga (ry p)), G_eill Sig0 (@app nat (@vec_map_list nat n (@vec_plus n v w) rx) Ga) (ry p) *)
    apply mm_sss_DEC0_inv in H1; auto.
(* Goal: G_eill Sig (@vec_map_list nat n v rx) (q i) *)
(* Goal: forall (n0 : nat) (_ : @eq nat (@vec_pos nat n v p) (S n0)), G_eill Sig (@vec_map_list nat n v rx) (q i) *)
    destruct H1; subst l w.
(* Goal: forall _ : G_eill Sig0 Ga (ry p), G_eill Sig0 (@app nat (@nil nat) Ga) (ry p) *)
(* Goal: forall (_ : @eq nat (@vec_pos nat n (@vec_one n r) p) O) (_ : G_eill Sig0 Ga (ry p)), G_eill Sig0 (@app nat (@vec_map_list nat n (@vec_one n r) rx) Ga) (ry p) *)
(* Goal: forall (_ : @eq nat (@vec_pos nat n (@vec_plus n v w) p) O) (_ : G_eill Sig0 Ga (ry p)), G_eill Sig0 (@app nat (@vec_map_list nat n (@vec_plus n v w) rx) Ga) (ry p) *)
    apply in_eill_fork with (ry p) (q j); auto.
(* Goal: @In eill_cmd (in_ll_cmd_dec (rx p) (q (Init.Nat.add (S O) i)) (q i)) Sig *)
(* Goal: G_eill Sig (@cons ll_vars (rx p) (@nil ll_vars)) (rx p) *)
    apply in_or_app; right.
(* Goal: @In eill_cmd (in_ll_cmd_dec (rx p) (q (Init.Nat.add (S O) i)) (q i)) SigI *)
(* Goal: G_eill Sig (@cons ll_vars (rx p) (@nil ll_vars)) (rx p) *)
    unfold SigI; destruct P as (ip,lP).
(* Goal: forall _ : G_eill Sig0 Ga (ry p), G_eill Sig0 (@app nat (@nil nat) Ga) (ry p) *)
(* Goal: forall (_ : @eq nat (@vec_pos nat n (@vec_one n r) p) O) (_ : G_eill Sig0 Ga (ry p)), G_eill Sig0 (@app nat (@vec_map_list nat n (@vec_one n r) rx) Ga) (ry p) *)
(* Goal: forall (_ : @eq nat (@vec_pos nat n (@vec_plus n v w) p) O) (_ : G_eill Sig0 Ga (ry p)), G_eill Sig0 (@app nat (@vec_map_list nat n (@vec_plus n v w) rx) Ga) (ry p) *)
    apply subcode_mm_linstr_dec with (1 := Hii); auto.
(* Goal: forall _ : G_eill Sig0 Ga (ry p), G_eill Sig0 (@app nat (@nil nat) Ga) (ry p) *)
(* Goal: forall (_ : @eq nat (@vec_pos nat n (@vec_one n r) p) O) (_ : G_eill Sig0 Ga (ry p)), G_eill Sig0 (@app nat (@vec_map_list nat n (@vec_one n r) rx) Ga) (ry p) *)
(* Goal: forall (_ : @eq nat (@vec_pos nat n (@vec_plus n v w) p) O) (_ : G_eill Sig0 Ga (ry p)), G_eill Sig0 (@app nat (@vec_map_list nat n (@vec_plus n v w) rx) Ga) (ry p) *)
    left; auto.
(* Goal: forall _ : G_eill Sig0 Ga (ry p), G_eill Sig0 (@app nat (@nil nat) Ga) (ry p) *)
(* Goal: forall (_ : @eq nat (@vec_pos nat n (@vec_one n r) p) O) (_ : G_eill Sig0 Ga (ry p)), G_eill Sig0 (@app nat (@vec_map_list nat n (@vec_one n r) rx) Ga) (ry p) *)
(* Goal: forall (_ : @eq nat (@vec_pos nat n (@vec_plus n v w) p) O) (_ : G_eill Sig0 Ga (ry p)), G_eill Sig0 (@app nat (@vec_map_list nat n (@vec_plus n v w) rx) Ga) (ry p) *)
    apply prop_5_2; auto.
    
(* Goal: forall (n0 : nat) (_ : @eq nat (@vec_pos nat n v p) (S n0)), G_eill Sig (@vec_map_list nat n v rx) (q i) *)
    intros u Hu.
(* Goal: forall _ : G_eill Sig0 Ga (ry p), G_eill Sig0 (@app nat (@nil nat) Ga) (ry p) *)
(* Goal: forall (_ : @eq nat (@vec_pos nat n (@vec_one n r) p) O) (_ : G_eill Sig0 Ga (ry p)), G_eill Sig0 (@app nat (@vec_map_list nat n (@vec_one n r) rx) Ga) (ry p) *)
(* Goal: forall (_ : @eq nat (@vec_pos nat n (@vec_plus n v w) p) O) (_ : G_eill Sig0 Ga (ry p)), G_eill Sig0 (@app nat (@vec_map_list nat n (@vec_plus n v w) rx) Ga) (ry p) *)
    apply mm_sss_DEC1_inv with (u := u) in H1; auto.
(* Goal: G_eill Sig (@vec_map_list nat n v rx) (q i) *)
    destruct H1; subst j w.
(* Goal: G_eill Sig (@vec_map_list nat n v rx) (q i) *)
    rewrite vec_change_pred with (1 := Hu).
(* Goal: G_eill Sig (@vec_map_list nat n (@vec_plus n (@vec_one n p) (@vec_change nat n v p u)) rx) (q i) *)
    apply in_eill_perm with (1 := Permutation_sym (vec_map_list_plus _ _ _)).
(* Goal: G_eill Sig (@app ll_vars (@vec_map_list ll_vars n (@vec_one n p) rx) (@vec_map_list ll_vars n (@vec_change nat n v p u) rx)) (q i) *)
    rewrite vec_map_list_one.
(* Goal: forall _ : G_eill Sig0 Ga (ry p), G_eill Sig0 (@app nat (@nil nat) Ga) (ry p) *)
(* Goal: forall (_ : @eq nat (@vec_pos nat n (@vec_one n r) p) O) (_ : G_eill Sig0 Ga (ry p)), G_eill Sig0 (@app nat (@vec_map_list nat n (@vec_one n r) rx) Ga) (ry p) *)
(* Goal: forall (_ : @eq nat (@vec_pos nat n (@vec_plus n v w) p) O) (_ : G_eill Sig0 Ga (ry p)), G_eill Sig0 (@app nat (@vec_map_list nat n (@vec_plus n v w) rx) Ga) (ry p) *)
    apply in_eill_dec with (rx p) (q (1+i)); auto.
(* Goal: @In eill_cmd (in_ll_cmd_dec (rx p) (q (Init.Nat.add (S O) i)) (q i)) Sig *)
(* Goal: G_eill Sig (@cons ll_vars (rx p) (@nil ll_vars)) (rx p) *)
    apply in_or_app; right.
(* Goal: @In eill_cmd (in_ll_cmd_dec (rx p) (q (Init.Nat.add (S O) i)) (q i)) SigI *)
(* Goal: G_eill Sig (@cons ll_vars (rx p) (@nil ll_vars)) (rx p) *)
    unfold SigI; destruct P as (ip,lP).
(* Goal: forall _ : G_eill Sig0 Ga (ry p), G_eill Sig0 (@app nat (@nil nat) Ga) (ry p) *)
(* Goal: forall (_ : @eq nat (@vec_pos nat n (@vec_one n r) p) O) (_ : G_eill Sig0 Ga (ry p)), G_eill Sig0 (@app nat (@vec_map_list nat n (@vec_one n r) rx) Ga) (ry p) *)
(* Goal: forall (_ : @eq nat (@vec_pos nat n (@vec_plus n v w) p) O) (_ : G_eill Sig0 Ga (ry p)), G_eill Sig0 (@app nat (@vec_map_list nat n (@vec_plus n v w) rx) Ga) (ry p) *)
    apply subcode_mm_linstr_dec with (1 := Hii); auto.
(* Goal: forall _ : G_eill Sig0 Ga (ry p), G_eill Sig0 (@app nat (@nil nat) Ga) (ry p) *)
(* Goal: forall (_ : @eq nat (@vec_pos nat n (@vec_one n r) p) O) (_ : G_eill Sig0 Ga (ry p)), G_eill Sig0 (@app nat (@vec_map_list nat n (@vec_one n r) rx) Ga) (ry p) *)
(* Goal: forall (_ : @eq nat (@vec_pos nat n (@vec_plus n v w) p) O) (_ : G_eill Sig0 Ga (ry p)), G_eill Sig0 (@app nat (@vec_map_list nat n (@vec_plus n v w) rx) Ga) (ry p) *)
    right; left; auto.
(* Goal: G_eill Sig (@cons ll_vars (rx p) (@nil ll_vars)) (rx p) *)
    apply in_eill_ax.
  Qed.
   
  Theorem G_eill_mm i v : P // (i,v) ->> (k,vec_zero) 
                      <-> Sig; vec_map_list v rx ⊦ q i.
  Proof.
(* Goal: iff (@sss_compute (mm_instr n) (vec nat n) (@mm_sss n) P (@pair nat (vec nat n) i v) (@pair nat (vec nat n) k (@vec_zero n))) (G_eill Sig (@vec_map_list nat n v rx) (q i)) *)
    split.
(* Goal: forall _ : @sss_compute (mm_instr n) (vec nat n) (@mm_sss n) P (@pair nat (vec nat n) i v) (@pair nat (vec nat n) k (@vec_zero n)), G_eill Sig (@vec_map_list nat n v rx) (q i) *)
(* Goal: forall _ : G_eill Sig (@vec_map_list nat n v rx) (q i), @sss_compute (mm_instr n) (vec nat n) (@mm_sss n) P (@pair nat (vec nat n) i v) (@pair nat (vec nat n) k (@vec_zero n)) *)
    apply lemma_5_3.
(* Goal: forall _ : G_eill Sig0 Ga (ry p), G_eill Sig0 (@app nat (@nil nat) Ga) (ry p) *)
(* Goal: forall (_ : @eq nat (@vec_pos nat n (@vec_one n r) p) O) (_ : G_eill Sig0 Ga (ry p)), G_eill Sig0 (@app nat (@vec_map_list nat n (@vec_one n r) rx) Ga) (ry p) *)
(* Goal: forall (_ : @eq nat (@vec_pos nat n (@vec_plus n v w) p) O) (_ : G_eill Sig0 Ga (ry p)), G_eill Sig0 (@app nat (@vec_map_list nat n (@vec_plus n v w) rx) Ga) (ry p) *)
    apply lemma_5_5; auto.
  Qed.
  
End Minsky.

