search

affeldt-aist / infotheo

A Coq formalization of information theory and linear error-correcting codes
GNU Lesser General Public License v2.1
64 stars 15 forks source link

ssrZ missing lemmas #65

Closed AyumuSaito closed 2 years ago

AyumuSaito commented 3 years ago 
Lemma intRD (n m : nat) : (n + m)%:Z = (n%:Z + m%:Z)%Z.
Proof. exact: Nat2Z.inj_add. Qed.

Lemma leZ0n (n : nat) : (0 <= n%:Z)%Z.
Proof. exact: Zle_0_nat. Qed.