Some lemmas about divisibility
Complete the following development:
Require Import Arith.
Definition divides (n m:nat) := exists p:nat, p*n = m.
Lemma divides_O : forall n:nat, divides n 0.
Lemma divides_plus : forall n m:nat, divides n m -> divides n (n+m).
Lemma not_divides_plus : forall n m:nat, ~ divides n m -> ~ divides n (n+m).
Lemma not_divides_lt : forall n m:nat, 0 m ~ divides n m.
Lemma not_lt_2_divides : forall n m:nat, n <> 1 -> n < 2 -> 0 < m ->
~ divides n m.
Lemma le_plus_minus : forall n m:nat, le n m -> m = n+(m-n).
Lemma lt_lt_or_eq : forall n m:nat, n < S m -> n
Solution
Look at this file
Going home
Pierre Castéran