Commit 40b18e24 by Robbert Krebbers

Unfolding properties for Nat.iter.

parent 0a1c37a3
 ... @@ -82,7 +82,7 @@ Proof. intros. destruct (Nat_mul_split_l n x2 x1 y2 y1); auto with lia. Qed. ... @@ -82,7 +82,7 @@ Proof. intros. destruct (Nat_mul_split_l n x2 x1 y2 y1); auto with lia. Qed. Notation lcm := Nat.lcm. Notation lcm := Nat.lcm. Notation divide := Nat.divide. Notation divide := Nat.divide. Notation "( x | y )" := (divide x y) : nat_scope. Notation "( x | y )" := (divide x y) : nat_scope. Instance divide_dec x y : Decision (x | y). Instance Nat_divide_dec x y : Decision (x | y). Proof. Proof. refine (cast_if (decide (lcm x y = y))); by rewrite Nat.divide_lcm_iff. refine (cast_if (decide (lcm x y = y))); by rewrite Nat.divide_lcm_iff. Defined. Defined. ... @@ -94,6 +94,11 @@ Hint Extern 0 (_ | _) => reflexivity. ... @@ -94,6 +94,11 @@ Hint Extern 0 (_ | _) => reflexivity. Lemma Nat_divide_ne_0 x y : (x | y) → y ≠ 0 → x ≠ 0. Lemma Nat_divide_ne_0 x y : (x | y) → y ≠ 0 → x ≠ 0. Proof. intros Hxy Hy ->. by apply Hy, Nat.divide_0_l. Qed. Proof. intros Hxy Hy ->. by apply Hy, Nat.divide_0_l. Qed. Lemma Nat_iter_S {A} n (f: A → A) x : Nat.iter (S n) f x = f (Nat.iter n f x). Proof. done. Qed. Lemma Nat_iter_S_r {A} n (f: A → A) x : Nat.iter (S n) f x = Nat.iter n f (f x). Proof. induction n; f_equal/=; auto. Qed. (** * Notations and properties of [positive] *) (** * Notations and properties of [positive] *) Open Scope positive_scope. Open Scope positive_scope. ... ...
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!