proposition: Lemma odd_oddsubn1 : forall n, n > 0 -> odd n.-1 = ~~odd n.
proof: Proof. induction n => //. destruct n => //. simpl. by case (odd n). Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool eqtype ssrnat seq fintype tuple zmodp div)