proposition: Lemma part_function_recip_pred_wd : pred_wd X R.
proof: Proof. red in |- *; intros x y H H0. elim H; intros H1 H2; split. apply (dom_wd X G x y H1 H0). intro H3; astepl (G x H1). auto. Qed.
imports: CoRN.algebra.CRings