proposition: Lemma minus_smaller_S: forall x y:nat, x - y < S x.
proof: Proof. intros x y; pattern y, x; elim x using nat_double_ind. destruct x0; auto with arith. simpl; auto with arith. simpl; auto with arith. Qed.
imports: Arith Vector List Extraction ZArith Compare_dec ZArith List