proposition: Lemma L1 : forall k i j b, Rgstar (quad b i j (S k)) (quad (S k + b) i j 0).
proof: Proof. induction k. simpl. constructor 1;auto. simpl. econstructor 3. econstructor 1; eauto. simpl in IHk. replace (S (S (k+b))) with (S (k + (S b))). apply IHk. auto with arith. Qed.
imports: Arith Omega Relations