proposition: Lemma L3 : forall b i j, Rgstar (quad b i (S j) 0) (quad (S (2 * b)) i j 0).
proof: Proof. intros. case b. simpl. econstructor 1. constructor. econstructor 3. econstructor 1; econstructor. replace (S (2* S n)) with ( S n + S (S n)). apply L1. omega. Qed.
imports: Arith Omega Relations