proposition: Lemma increasing_geq_minus (n k : nat) : increasing_geq n (n - k).
proof: Proof. simple_induction k k IHk. - destruct (symmetric_paths _ _ (sub_n_0 n)); constructor. - destruct (@leq_dichot n k) as [l | g]. + destruct (symmetric_paths _ _ (sub_leq_0 _ _ _)) in IHk. apply leq_S in l. destruct (symmetric_paths _ _ (sub_leq_0 _ _ _)). exact IHk. + change k.+1 with (1 + k). destruct (nat_add_comm k 1). destruct (symmetric_paths _ _ (subsubadd n k 1)). destruct (symmetric_paths _ _ (@predeqminus1 (n - k))). apply increasing_geq_S. unfold ">", "<" in *. apply lt_sub_gt_0 in g. now (destruct (symmetric_paths _ _ (S_predn (n - k) 0 _))). Defined.
imports: Basics Spaces.Nat.Core