proposition: Lemma minus_n_Sk : forall n k : nat, k < n -> n - k = S (n - S k).
proof: Proof. intros n k Hlt. induction n as [| n Hrecn]. inversion Hlt. rewrite <- Nat.sub_succ_l. simpl in |- *. reflexivity. unfold lt in Hlt. inversion Hlt. auto. apply (le_trans (S k)). auto. assumption. Qed.
imports: Coq.ZArith.ZArith CoRN.logic.CLogic Coq(Lia)