proposition: Lemma BigNdiv : div_theory BigN.eq BigN.add BigN.mul (@id _) (fun a b => if b =? 0 then (0,a) else BigN.div_eucl a b).
proof: Proof. constructor. unfold id. intros a b. BigN.zify. case Z.eqb_spec. BigN.zify. auto with zarith. intros NEQ. generalize (BigN.spec_div_eucl a b). generalize (Z_div_mod_full (BigN.to_Z a) (BigN.to_Z b) NEQ). destruct BigN.div_eucl as (q,r), Z.div_eucl as (q',r'). intros (EQ,_). injection 1 as EQr EQq. BigN.zify. rewrite EQr, EQq; auto. Qed.
imports: Lia CyclicAxioms Ring63 NSig NSigNAxioms NMake NProperties GenericMinMax