proposition: Proposition natsubreflectsleq { n m k : nat } : k <= m -> n - k <= m - k -> n <= m.
proof: Proof. intros ineq1 ineq2. apply (@nataddpreservesleq _ _ k) in ineq2. apply (@leq_trans _ (n - k + k) _ (natminusplusineq _ _)). apply (@leq_trans _ (m - k + k) _ _). destruct (symmetric_paths _ _ (natminuspluseq k m ineq1)); easy. Defined.
imports: Basics Spaces.Nat.Core