proposition: Lemma R_recip_inverse : forall x x_, x[*]R_recip x x_ [=] [1].
proof: Proof. intros x Hx; elim Hx; intro Hlt; elim Hlt; intros N HN; elim HN; clear Hx Hlt HN; simpl in |- *; intros e He HN Hap; elim Hap; intro Hlt; elim Hlt; intros K HK; elim HK; clear Hap Hlt HK; intros d Hd HM; simpl in HM. apply (less_irreflexive_unfolded _ d). apply leEq_less_trans with ([0]:F); auto. simpl in HM. eapply leEq_wdr. apply (HM (Nat.max K N)); auto with arith. unfold CS_seq_recip_seq in |- *; elim lt_le_dec; intro. exfalso; apply Nat.le_ngt with N (Nat.max K N); auto with arith. simpl in |- *; rational. apply (less_irreflexive_unfolded _ d). apply leEq_less_trans with ([0]:F); auto. simpl in HM. eapply leEq_wdr. apply (HM (Nat.max K N)); auto with arith. unfold CS_seq_recip_seq in |- *; elim lt_le_dec; intro. exfalso; apply Nat.le_ngt with N (Nat.max K N); auto with arith. simpl in |- *; rational. apply (less_irreflexive_unfolded _ d). apply leEq_less_trans with ([0]:F); auto. simpl in HM. eapply leEq_wdr. apply (HM (Nat.max K N)); auto with arith. unfold CS_seq_recip_seq in |- *; elim lt_le_dec; intro. exfalso; apply Nat.le_ngt with N (Nat.max K N); auto with arith. simpl in |- *; rational. apply (less_irreflexive_unfolded _ d). apply leEq_less_trans with ([0]:F); auto. simpl in HM. eapply leEq_wdr. apply (HM (Nat.max K N)); auto with arith. unfold CS_seq_recip_seq in |- *; elim lt_le_dec; intro. exfalso; apply Nat.le_ngt with N (Nat.max K N); auto with arith. simpl in |- *; rational. Qed.
imports: CoRN.algebra.COrdCauchy CoRN.tactics.RingReflection