proposition: Lemma Build_Ctype_comp : forall x x' y y' : R, Equal x x' -> Equal y y' -> Equal (s:=Cset) (Build_Ctype x y) (Build_Ctype x' y').
proof: Proof. intros x x' y y' H' H'0; try assumption. simpl in |- *. red in |- *; auto with algebra. Qed.
imports: Cfield_facts Ring_util