proposition: Theorem not_le_Sn_0 : forall n:nat, ~ (S n <= 0).
proof: Proof. red; intros n H. case H. Abort. Lemma not_le_Sn_0_with_constraints : forall n p , S n <= p -> p = 0 -> False. Proof. intros n p H; case H ; intros; discriminate. Qed.
imports: Arith Vector List Extraction ZArith Compare_dec ZArith List