proposition: Lemma Cnorm_sqr_pos_lt : forall r r1 : R, (r,r1) <> C0 -> 0 < r * r + r1 * r1.
proof: Proof. intros r r1 z_neq_0. case (proj1 (C0_neq_R0_neq _) z_neq_0) ; simpl ; intro H. apply Rplus_lt_le_0_compat. apply Rsqr_pos_lt ; assumption. apply Rle_0_sqr. apply Rplus_le_lt_0_compat. apply Rle_0_sqr. apply Rsqr_pos_lt ; assumption. Qed.
imports: Ctacfield Cbase Cpow Lia