proposition: Theorem my_Cle_ind : forall (n : nat) (P : nat -> CProp), P n -> (forall m : nat, Cle n m -> P m -> P (S m)) -> forall n0 : nat, Cle n n0 -> P n0.
proof: Proof. intros n P. generalize (Cle_rect n (fun (n0 : nat) (H : Cle n n0) => P n0)); intro. assumption. Qed.
imports: Coq.Arith.Compare_dec CoRN.logic.CornBasics Coq.ZArith.ZArith Coq.setoid_ring.ZArithRing Coq.Arith.Wf_nat Coq(Lia)