proposition: Lemma minus_smaller_positive : forall x y:nat, x <>0 -> y <> 0 -> x - y < x.
proof: Proof. destruct x; destruct y; ( simpl;intros; apply minus_smaller_S || intros; absurd (0=0); auto). Qed.
imports: Arith Vector List Extraction ZArith Compare_dec ZArith List