proposition: Lemma mod_nat_correct: forall (k l:nat)(H:(l>0)%Z), (k mod l)%Z = (Z_of_nat (mod_nat k l H)).
proof: Proof. intros k l H. unfold mod_nat. unfold sum_rec. unfold sum_rect. case ( Zmod_pos k l H). tauto. unfold sigT_rec. unfold sigT_rect. intro H0. case H0. simpl. intro x. set (H1:= (inject_nat_convert x)). intuition. Qed.
imports: CoRN.model.Zmod.ZMod CoRN.logic.CLogic