proposition: Lemma test : 10000%num * 10000%num * (99999999%num + 1) = 10000000000000000%num.
proof: Proof. by rewrite [X in X = _]RnatE; compute; reflexivity. Qed.
imports: ZArith Lia mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div seq zmodp) mathcomp(path choice fintype tuple finset ssralg ssrnum bigop ssrint) CoqEAL(hrel param refinements pos)