Commit 6c0480f2 authored by Jacques-Henri Jourdan's avatar Jacques-Henri Jourdan Committed by Guillaume Melquiond

Move cond_Zopp to Fcore_Zaux.

parent 2e32d89f
......@@ -1897,9 +1897,8 @@ Qed.
End Bool.
Section cond_opp.
Section cond_Ropp.
Definition cond_Zopp (b : bool) m := if b then Zopp m else m.
Definition cond_Ropp (b : bool) m := if b then Ropp m else m.
Theorem Z2R_cond_Zopp :
......@@ -1911,15 +1910,6 @@ apply Z2R_opp.
apply refl_equal.
Qed.
Theorem abs_cond_Zopp :
forall b m,
Zabs (cond_Zopp b m) = Zabs m.
Proof.
intros [|] m.
apply Zabs_Zopp.
apply refl_equal.
Qed.
Theorem abs_cond_Ropp :
forall b m,
Rabs (cond_Ropp b m) = Rabs m.
......@@ -1929,18 +1919,6 @@ apply Rabs_Ropp.
apply refl_equal.
Qed.
Theorem cond_Zopp_Zlt_bool :
forall m,
cond_Zopp (Zlt_bool m 0) m = Zabs m.
Proof.
intros m.
apply sym_eq.
case Zlt_bool_spec ; intros Hm.
apply Zabs_non_eq.
now apply Zlt_le_weak.
now apply Zabs_eq.
Qed.
Theorem cond_Ropp_Rlt_bool :
forall m,
cond_Ropp (Rlt_bool m 0) m = Rabs m.
......@@ -2015,4 +1993,4 @@ apply Ropp_plus_distr.
apply refl_equal.
Qed.
End cond_opp.
End cond_Ropp.
......@@ -745,3 +745,30 @@ apply Zlt_gt.
Qed.
End Zcompare.
Section cond_Zopp.
Definition cond_Zopp (b : bool) m := if b then Zopp m else m.
Theorem abs_cond_Zopp :
forall b m,
Zabs (cond_Zopp b m) = Zabs m.
Proof.
intros [|] m.
apply Zabs_Zopp.
apply refl_equal.
Qed.
Theorem cond_Zopp_Zlt_bool :
forall m,
cond_Zopp (Zlt_bool m 0) m = Zabs m.
Proof.
intros m.
apply sym_eq.
case Zlt_bool_spec ; intros Hm.
apply Zabs_non_eq.
now apply Zlt_le_weak.
now apply Zabs_eq.
Qed.
End cond_Zopp.
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment