proposition: Lemma BigZdiv : div_theory BigZ.eq BigZ.add BigZ.mul (@id _) (fun a b => if b =? 0 then (0,a) else BigZ.div_eucl a b).
proof: Proof. constructor. unfold id. intros a b. BigZ.zify. case Z.eqb_spec. BigZ.zify. auto with zarith. intros NEQ. generalize (BigZ.spec_div_eucl a b). generalize (Z_div_mod_full (BigZ.to_Z a) (BigZ.to_Z b) NEQ). destruct BigZ.div_eucl as (q,r), Z.div_eucl as (q',r'). intros (EQ,_). injection 1 as EQr EQq. BigZ.zify. rewrite EQr, EQq; auto. Qed.
imports: BigN ZProperties ZDivFloor ZSig ZSigZAxioms ZMake Ring Lia