proposition: Lemma nrCC3_a4 : degree_le 1 (_X_[+]_C_ II).
proof: Proof. apply degree_imp_degree_le. cut (degree 1 (_C_ II[+]_X_)); intros. apply (degree_wd _ (_C_ II[+]_X_)). apply cag_commutes_unfolded. rename X into H. exact H. apply (degree_plus_rht _ (_C_ II) _X_ 0 1). apply degree_le_c_. apply degree_x_. auto with arith. Qed.
imports: CoRN.complex.CComplex Coq.Arith.Wf_nat Coq.setoid_ring.ArithRing