proposition: Lemma Cadd_eq_reg_l : forall z z1 z2, z + z1 = z + z2 -> z1 = z2.
proof: Proof. intros z z1 z2 H. destruct z as (r, r0) ; destruct z1 as (r1, r2) ; destruct z2 as (r3, r4). simpl in *. apply ( (Ceq _ _)) in H. destruct H. simpl in *. apply Rplus_eq_reg_l in H. apply Rplus_eq_reg_l in H0. rewrite H; rewrite H0. reflexivity. Qed.
imports: Ctacfield Cbase Cpow Lia