proposition: Proposition natsubpreservesleq { n m k : nat } : n <= m -> n - k <= m - k.
proof: Proof. simple_induction k k IHk. - destruct (symmetric_paths _ _ (sub_n_0 n)), (symmetric_paths _ _ (sub_n_0 m)); done. - intro l. change (k.+1) with (1 + k). destruct (nat_add_comm k 1). destruct (symmetric_paths _ _ (subsubadd n k 1)). destruct (symmetric_paths _ _ (subsubadd m k 1)). destruct (symmetric_paths _ _ (@predeqminus1 (n -k))). destruct (symmetric_paths _ _ (@predeqminus1 (m -k))). apply leq_n_pred, IHk. exact l. Defined.
imports: Basics Spaces.Nat.Core