proposition: Lemma intR_addbit m : m == (m %% 2%N)%Z + 2 * (m %/ 2%N)%Z.
proof: Proof. by rewrite {1}(divz_eq m 2%:Z) mulRC addRC intRD intRM. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div order) mathcomp(ssralg ssrnum ssrint rat intdiv) Coq(Morphisms Setoid) fourcolor(real realsyntax)