proposition: Lemma predecessor_of_positive : forall n, 1 <= n -> exists p:nat, n = S p.
proof: Proof. intros n H; case H. - exists 0; trivial. - intros m Hm; exists m;trivial. Qed.
imports: Arith Vector List Extraction ZArith Compare_dec