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