proposition: Lemma Rabs_n_min_m : forall m n : ℕ, (m <= n)%nat -> | n - m | = n - m.
proof: Proof. Take m, n : nat. Assume that (m <= n)%nat. It holds that (m <= n). We conclude that (| n - m | = n - m). Qed.
imports: Coq.Reals.Reals Tactics Automation Libs.Negation Notations