proposition: Lemma StepQeq_bool_correct : forall x y, StepQeq_bool x y = true -> x == y.
proof: Proof. intros x y H. destruct StepQsrt. rewrite <- (Radd_0_l x). rewrite <- (Ropp_def y). transitivity (y + (constStepF (0:QS))). set (z:=constStepF (X:=QS) 0). rewrite <- (Radd_assoc). apply StepQplus_wd. reflexivity. rewrite -> Radd_comm. rewrite <- Rsub_def. unfold StepF_eq. revert H. unfold StepQeq_bool. generalize (x-y). intros s H. induction s. apply: Qeq_bool_eq;assumption. symmetry in H. destruct (andb_true_eq _ _ H) as [H1 H2]. split. apply IHs1; symmetry; assumption. apply IHs2; symmetry; assumption. rewrite -> Radd_comm. apply Radd_0_l. Qed.
imports: CoRN.algebra.RSetoid CoRN.model.metric2.Qmetric Coq.QArith.QArith CoRN.metric2.StepFunctionSetoid Coq.QArith.Qabs Coq.Bool.Bool CoRN.tactics.CornTac CoRN.logic.CornBasics CoRN.algebra.RSetoid