proposition: Lemma not_circular : forall n:nat, n <> S n.
proof: Proof. intro n. apply nat_ind with (P:= fun n => n <> S n). discriminate. red; intros n0 Hn0 eqn0Sn0;injection eqn0Sn0;trivial. Qed.
imports: Arith Vector List Extraction ZArith Compare_dec ZArith List