proposition: Lemma Cre_inv_compat_0 : forall z, Cre z = 0%R -> Cre (/z) = 0%R.
proof: Proof. intuition. destruct z. unfold Cinv. simpl in H. rewrite H. unfold Rdiv. rewrite Rmult_0_l. reflexivity. Qed.
imports: Ctacfield Cbase Cpow Lia