proposition: Lemma minus_n_minus_n_k : forall k n : nat, k <= n -> k = n - (n - k).
proof: Proof. intros k n Hle. induction k as [| k Hreck]. rewrite Nat.sub_0_r. symmetry in |- *. apply Nat.sub_diag. set (K := k) in |- * at 2. rewrite Hreck. unfold K in |- *; clear K. rewrite (minus_n_Sk n k). rewrite (minus_n_Sk n (n - S k)). reflexivity. unfold lt in |- *. rewrite <- (minus_n_Sk n k). apply le_minus. unfold lt in |- *. exact Hle. unfold lt in |- *. exact Hle. apply (le_trans (S k)). auto. exact Hle. Qed.
imports: Coq.ZArith.ZArith CoRN.logic.CLogic Coq(Lia)