proposition: Lemma le_pred : forall n m : nat, n <= m -> pred n <= pred m.
proof: Proof. simple induction n. simpl in |- *. auto with arith. intros n0 Hn0. simple induction m. simpl in |- *. intro H. inversion H. intros n1 H H0. simpl in |- *. auto with arith. Qed.
imports: Coq(Lia) CoRN.stdlib_omissions.List Coq.Logic.Eqdep_dec Coq.Setoids.Setoid