diff options
Diffstat (limited to 'theories')
| -rw-r--r-- | theories/Arith/Div2.v | 7 |
1 files changed, 7 insertions, 0 deletions
diff --git a/theories/Arith/Div2.v b/theories/Arith/Div2.v index a6782c5f8c..b05eaa77d8 100644 --- a/theories/Arith/Div2.v +++ b/theories/Arith/Div2.v @@ -106,6 +106,13 @@ Proof. Intro. Unfold double. Simpl. Auto with arith. Qed. +Lemma double_plus : (m,n:nat) (double (plus m n))=(plus (double m) (double n)). +Proof. +Intros m n. Unfold double. +Do 2 Rewrite -> plus_assoc_r. Rewrite -> (plus_permute n). +Reflexivity. +Qed. + Hints Resolve double_S : arith. Lemma even_odd_double : (n:nat) |