The Coq mailing list

[AUGER C�dric <Cedric.Auger AT lri.fr>]

I was wrong, fact is finally easier than prod_list, but the admitted
lemmas are quite long and boring to prove...

Record Divides (n m : nat) : Prop :=
Div { quo : nat;
      div_spe : m = n * quo
    }.

Record Prime (n : nat) : Prop :=
{ one_is_not_prime : n <> 1;
  no_other_prime_factor : forall q : nat, q<>1 -> q<>n ->
                          forall m, n = q * m -> False
}.

Fixpoint fact (n:nat) : nat :=
   match n with
     | O => 1
     | S n => (S n) * fact n
   end.

Lemma L2 : forall m n, n <= m -> n <> 0 -> Divides n (fact m).
Proof.
 intros m n H; induction H.
  destruct n.
   intro K; destruct K; split.
  intros _.
  split with (fact n).
  reflexivity.
 intro K; destruct (IHle K).
 split with ((S m) * quo).
 simpl.
 rewrite div_spe.
 rewrite mult_plus_distr_l.
 rewrite mult_assoc.
 rewrite (mult_comm m).
 rewrite mult_assoc.
 split.
Qed.

Lemma L3 : forall m n, n <> 1 -> Divides n m -> Divides n (S m) ->
           False.
Proof.
 admit.
Qed.

Lemma L4 : forall m, exists n, Prime n /\ exists o, m = n * o.
Proof.
 admit.
Qed.

Theorem Euclide : forall (y:nat) ,
       (forall x:nat , Prime(x) -> gt x y -> False) -> False.
Proof.
 intros.
 destruct (L4 (S (fact y))) as [d [Hp [o Heq]]].
 destruct (le_lt_dec d y).
 refine (L3 _ _ _ (L2 _ _ l _) _).
 destruct Hp; easy.
 destruct d; simpl in *;[|intro K]; discriminate.
 split with o.
 assumption.
 exact (H _ Hp l).
Qed.