(n k : nat) : increasing_geq n (n - k). Proof. simple_induction k k IHk. - destruct (symmetric_paths _ _ (nat_sub_zero_r n)); constructor. - destruct (@leq_dichotomy n k) as [l | g]. + destruct (equiv_nat_sub_leq _)^ in IHk. apply leq_succ_r in l. destruct (equiv_nat_sub_leq _)^. exact IHk. + change k.+1 with (1 + k). destruct (nat_add_comm k 1). destruct (symmetric_paths _ _ (nat_sub_r_add n k 1)). destruct (symmetric_paths _ _ (@predeqminus1 (n - k))). apply increasing_geq_S. unfold ">", "<" in *. apply equiv_lt_lt_sub in g. by (destruct (symmetric_paths _ _ (nat_succ_pred (n - k) _))). Defined.
Require Import Basics. Require Import Spaces.Nat.Core.