proposition: Lemma mod_a_a_0 : forall a, a mod a = N0.
proof: Proof. intros a;generalize (div_eucl_spec a a);rewrite <- Pmod_div_eucl. destruct (fst (a / a));unfold Z_of_N at 1. rewrite Zmult_0_l;intros (H1,H2);exfalso;lia. assert (a<=p*a). pattern (Zpos a) at 1;rewrite <- (Zmult_1_l a). assert (H1:= Zlt_0_pos p);assert (H2:= Zle_0_pos a); apply Zmult_le_compat;trivial;try lia. destruct (a mod a)%P;auto with zarith. unfold Z_of_N;assert (H1:= Zlt_0_pos p0);intros (H2,H3);exfalso;lia. Qed.
imports: ZArith Lia ZCmisc