proposition: Lemma imag_comp : forall x x' : Cset, Equal x x' -> Equal (imag x) (imag x').
proof: Proof. simpl in |- *. unfold Ceq in |- *. intros x x' H'; elim H'; intros H'0 H'1; try exact H'1; clear H'. Qed.
imports: Cfield_facts Ring_util