proposition: Lemma natlike_ind : forall P:Z -> Prop, P 0 -> (forall x:Z, 0 <= x -> P x -> P (Z.succ x)) -> forall x:Z, 0 <= x -> P x.
proof: Proof. intros P Ho Hrec x Hx; apply Z_of_nat_prop; trivial. intros n; induction n. - exact Ho. - rewrite Nat2Z.inj_succ. apply Hrec; trivial using Nat2Z.is_nonneg. Qed.
imports: BinInt Zcompare Zorder Znat Zmisc Wf_nat