Commit d4eae082 authored by Martin PORTALIER's avatar Martin PORTALIER

Update facts.v

parent 554bd584
Pipeline #19218 failed with stages
in 2 minutes and 20 seconds
......@@ -144,3 +144,18 @@ Require Import List Classical_Prop Classical_Pred_Type.
Proof.
move => m n p H_inf. ssromega.
Qed.
Lemma sum_inf_3: forall k m p,
0 < p -> k + m <= k + m + p - 1.
Proof.
move => k m p H_pos. ssromega.
Qed.
Lemma inf_less1: forall n m p,
0 < m -> m * n < p + n -> (m - 1) * n < p.
Proof.
move => n m p. destruct m as [|m]; auto.
have ->: (succn m - 1) = m by ssromega.
have ->: succn m * n = m * n + n by ssromega.
rewrite ltn_add2r. auto.
Qed.
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment