-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathmonotone_div2.v
59 lines (51 loc) · 1.46 KB
/
monotone_div2.v
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
Require Import Div2.
Require Import Even.
Require Import Omega.
Lemma monotone_double_double_r : forall m n, double m <= double n -> m <= n .
unfold double.
intros.
induction m; induction n; intros; simpl; try omega; try eauto.
Qed.
Lemma monotone_Sdouble_double_r : forall m n, S (double m) <= double n -> m <= n .
unfold double.
intros.
induction m; induction n; intros; simpl; try omega; try eauto.
Qed.
Lemma monotone_double_Sdouble_r : forall m n, double m <= S (double n) -> m <= n .
unfold double.
intros.
induction m; induction n; intros; simpl; try omega; try eauto.
Qed.
Lemma monotone_Sdouble_Sdouble_r : forall m n, S (double m) <= S (double n) -> m <= n .
unfold double.
intros.
induction m; induction n; intros; simpl; try omega; try eauto.
Qed.
Lemma monotone_div2 : forall m n, m <= n -> div2 m <= div2 n.
Proof.
intros.
generalize (even_odd_dec m).
generalize (even_odd_dec n).
intros.
destruct H0.
generalize (even_double n e); intro.
destruct H1.
generalize (even_double m e0); intro.
rewrite H0,H1 in H.
apply monotone_double_double_r.
apply H.
generalize (odd_double m o); intro.
rewrite H0,H1 in H.
apply monotone_Sdouble_double_r.
apply H.
generalize (odd_double n o); intro.
destruct H1.
generalize (even_double m e); intro.
rewrite H0,H1 in H.
apply monotone_double_Sdouble_r.
apply H.
generalize (odd_double m o0); intro.
rewrite H0,H1 in H.
apply monotone_Sdouble_Sdouble_r.
apply H.
Qed.