lemma div2SO: ∀n,q. div2 n = 〈q,ff〉 → div2 (S n) = 〈q,tt〉.
#n #q #H normalize >H normalize // qed.
lemma div2S1: ∀n,q. div2 n = 〈q,tt〉 → div2 (S n) = 〈S q,ff〉.
#n #q #H normalize >H normalize // qed.
lemma div2SO: ∀n,q. div2 n = 〈q,ff〉 → div2 (S n) = 〈q,tt〉.
#n #q #H normalize >H normalize // qed.
lemma div2S1: ∀n,q. div2 n = 〈q,tt〉 → div2 (S n) = 〈S q,ff〉.
#n #q #H normalize >H normalize // qed.