-(*it's a generalization of the existing theorem divides_gcd_aux (in which
- c = 1), proved in file gcd.ma
- *)
-theorem divides_times_gcd_aux: \forall p,m,n,d,c.
-O \lt c \to O < n \to n \le m \to n \le p \to
-d \divides (c*m) \to d \divides (c*n) \to d \divides c*gcd_aux p m n.
-intro.
-elim p
-[ absurd (O < n)
- [ assumption
- | apply le_to_not_lt.
- assumption
- ]
-| simplify.
- cut (n1 \divides m \lor n1 \ndivides m)
- [ elim Hcut
- [ rewrite > divides_to_divides_b_true
- [ simplify.
- assumption
- | assumption
- | assumption
- ]
- | rewrite > not_divides_to_divides_b_false
- [ simplify.
- apply H
- [ assumption
- | cut (O \lt m \mod n1 \lor O = m \mod n1)
- [ elim Hcut1
- [ assumption
- | absurd (n1 \divides m)
- [ apply mod_O_to_divides
- [ assumption
- | apply sym_eq.
- assumption
- ]
- | assumption
- ]
- ]
- | apply le_to_or_lt_eq.
- apply le_O_n
- ]
- | apply lt_to_le.
- apply lt_mod_m_m.
- assumption
- | apply le_S_S_to_le.
- apply (trans_le ? n1)
- [ change with (m \mod n1 < n1).
- apply lt_mod_m_m.
- assumption
- | assumption
- ]
- | assumption
- | rewrite < times_mod
- [ rewrite < (sym_times c m).
- rewrite < (sym_times c n1).
- apply divides_mod
- [ rewrite > (S_pred c)
- [ rewrite > (S_pred n1)
- [ apply (lt_O_times_S_S)
- | assumption
- ]
- | assumption
- ]
- | assumption
- | assumption
- ]
- | assumption
- | assumption
- ]
- ]
- | assumption
- | assumption
- ]
- ]
- | apply (decidable_divides n1 m).
- assumption
- ]
-]
-qed.
-
-(*it's a generalization of the existing theorem divides_gcd_d (in which
- c = 1), proved in file gcd.ma
- *)
-theorem divides_d_times_gcd: \forall m,n,d,c.
-O \lt c \to d \divides (c*m) \to d \divides (c*n) \to d \divides c*gcd n m.
-intros.
-change with
-(d \divides c *
-match leb n m with
- [ true \Rightarrow
- match n with
- [ O \Rightarrow m
- | (S p) \Rightarrow gcd_aux (S p) m (S p) ]
- | false \Rightarrow
- match m with
- [ O \Rightarrow n
- | (S p) \Rightarrow gcd_aux (S p) n (S p) ]]).
-apply (leb_elim n m)
-[ apply (nat_case1 n)
- [ simplify.
- intros.
- assumption
- | intros.
- change with (d \divides c*gcd_aux (S m1) m (S m1)).
- apply divides_times_gcd_aux
- [ assumption
- | unfold lt.
- apply le_S_S.
- apply le_O_n
- | assumption
- | apply (le_n (S m1))
- | assumption
- | rewrite < H3.
- assumption
- ]
- ]
-| apply (nat_case1 m)
- [ simplify.
- intros.
- assumption
- | intros.
- change with (d \divides c * gcd_aux (S m1) n (S m1)).
- apply divides_times_gcd_aux
- [ unfold lt.
- change with (O \lt c).
- assumption
- | apply lt_O_S
- | apply lt_to_le.
- apply not_le_to_lt.
- assumption
- | apply (le_n (S m1)).
- | assumption
- | rewrite < H3.
- assumption
- ]
- ]
-]
-qed.
-
-(* 2 basic properties of divides predicate *)
-theorem aDIVb_to_bDIVa_to_aEQb:
-\forall a,b:nat.
-a \divides b \to b \divides a \to a = b.
-intros.
-apply antisymmetric_divides;
- assumption.
-qed.
-
-
-theorem O_div_c_to_c_eq_O: \forall c:nat.
-O \divides c \to c = O.
-intros.
-apply aDIVb_to_bDIVa_to_aEQb
-[ apply divides_n_O
-| assumption
-]
-qed.
-