The Coq mailing list

[Laurent Théry <Laurent.Thery AT inria.fr>]

Hi,

your example is ok, you've just forgot to prove your lemma my_r_th:


(*****************************************************)
Lemma my_r_th : semi_ring_theory origin (next origin) my_r_plus 
my_r_mult (@eq my_r).
Proof.
admit.
Qed.

Add Ring my_r : my_r_th.


(* This works! *)
Goal forall x, my_r_plus x origin = x.
intros.
ring.

(*****************************************************)


Now to prove my_r_th starts with


(*****************************************************)

Lemma my_r_th : semi_ring_theory origin (next origin) my_r_plus 
my_r_mult (@eq my_r).
Proof.
split.

(*****************************************************)

and you see what you have to prove.