Commit faa676b0 authored by Claude Marche's avatar Claude Marche

compatibility coq 8.4

parent 17dc1488
......@@ -13,7 +13,7 @@ Lemma infix_lseq_Zle :
forall x y, infix_lseq x y <-> Zle x y.
Proof.
intros x y.
apply iff_Symmetric.
apply iff_sym.
apply Zle_lt_or_eq_iff.
Qed.
......
......@@ -102,4 +102,3 @@ replace 1%R with (1*1)%R by auto with real.
apply Rmult_le_compat; auto with real.
Qed.
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