proposition: Lemma invariantS_algo m n p q : invariant_algo m.+1 n p q <-> invariant_algo m n (left (m + n) p) (left_poly (2 ^ (m + n)) q) /\ invariant_algo m n (right (m + n) p) (right_poly (2 ^ (m + n)) q).
proof: Proof. by []. Qed.
imports: mathcomp(all_ssreflect all_algebra ssrnum)