diff options
Diffstat (limited to 'src/Util/ZUtil/Morphisms.v')
| -rw-r--r-- | src/Util/ZUtil/Morphisms.v | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/src/Util/ZUtil/Morphisms.v b/src/Util/ZUtil/Morphisms.v index e0ab179a8..285fa5261 100644 --- a/src/Util/ZUtil/Morphisms.v +++ b/src/Util/ZUtil/Morphisms.v @@ -46,4 +46,6 @@ Module Z. Proof. intros ???; apply Z.pow_le_mono_r; try reflexivity; try assumption. Qed. Lemma add_with_carry_le_Proper : Proper (Z.le ==> Z.le ==> Z.le ==> Z.le) Z.add_with_carry. Proof. unfold Z.add_with_carry; repeat (omega || intro). Qed. + Lemma sub_with_borrow_le_Proper : Proper (Basics.flip Z.le ==> Z.le ==> Basics.flip Z.le ==> Z.le) Z.sub_with_borrow. + Proof. unfold Z.sub_with_borrow, Z.add_with_carry, Basics.flip; repeat (omega || intro). Qed. End Z. |