proposition: Lemma odd_power_cancel_pos : forall n, Nat.Odd n -> forall x : R, [0] [<] x[^]n -> [0] [<] x.
proof: Proof. intros n [m Hm]%to_Codd x. simpl. intros H. apply mult_pos_imp in H as [[H1 H2] | [H1 H2]]. - exact H2. - exfalso. apply less_imp_ap in H2. apply (even_power_pos m) in H2; [| now apply Ceven_to]. apply less_antisymmetric_unfolded with (1 := H1). exact H2. Qed.
imports: CoRN.algebra.COrdFields Coq(Lia)