proposition: Lemma mulc_WW_spec : forall x y, Φ ( x *c y ) = φ x * φ y.
proof: Proof. intros x y;unfold mulc_WW. generalize (mulc_spec x y);destruct (mulc x y);simpl;intros Heq;rewrite Heq. case_eq (is_zero i);intros;trivial. apply is_zero_spec in H;rewrite H, to_Z_0. case_eq (is_zero i0);intros;trivial. apply is_zero_spec in H0;rewrite H0, to_Z_0, Zmult_comm;trivial. Qed.
imports: CyclicAxioms ZArith Uint63