We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
1 parent d2b6880 commit 813bc57Copy full SHA for 813bc57
theories/Classes/orders/naturals.v
@@ -59,7 +59,7 @@ etransitivity.
59
- apply pos_ge_1.
60
Qed.
61
62
-#[export] Instance OrderReflecting_left_mult : forall (z : N), PropHolds (z <> 0) -> OrderReflecting (z *.).
+#[export] Instance orderreflecting_left_mult : forall (z : N), PropHolds (z <> 0) -> OrderReflecting (z *.).
63
Proof.
64
intros z ?. red. apply (order_reflecting_pos (.*.) z).
65
apply nat_ne_0_pos. trivial.
0 commit comments