proposition: Theorem Cle_n_S : forall n m : nat, Cle n m -> Cle (S n) (S m).
proof: Proof. intros n m H. pattern m in |- *. apply (my_Cle_ind n). apply Cle_n. intros. apply Cle_S. assumption. assumption. Qed.
imports: Coq.Arith.Compare_dec CoRN.logic.CornBasics Coq.ZArith.ZArith Coq.setoid_ring.ZArithRing Coq.Arith.Wf_nat Coq(Lia)